| author | huffman |
| Sat, 21 Apr 2012 13:49:31 +0200 | |
| changeset 48524 | f7df7104d13e |
| parent 48339 | 214bfaae738d |
| child 49043 | a5377f6d9f14 |
| permissions | -rw-r--r-- |
1 (* Title: HOL/ex/ROOT.ML
3 Miscellaneous examples for Higher-Order Logic.
4 *)
6 no_document use_thys [
7 "~~/src/HOL/Library/State_Monad",
8 "Code_Nat_examples",
9 "~~/src/HOL/Library/FuncSet",
10 "Eval_Examples",
11 "Normalization_by_Evaluation",
12 "Hebrew",
13 "Chinese",
14 "Serbian"
15 ];
17 use_thys [
18 "Iff_Oracle",
19 "Coercion_Examples",
20 "Numeral_Representation",
21 "Higher_Order_Logic",
22 "Abstract_NAT",
23 "Guess",
24 "Binary",
25 "Fundefs",
26 "Induction_Schema",
27 "LocaleTest2",
28 "Records",
29 "While_Combinator_Example",
30 "MonoidGroup",
31 "BinEx",
32 "Hex_Bin_Examples",
33 "Antiquote",
34 "Multiquote",
35 "PER",
36 "NatSum",
37 "ThreeDivides",
38 "Intuitionistic",
39 "CTL",
40 "Arith_Examples",
41 "BT",
42 "Tree23",
43 "MergeSort",
44 "Lagrange",
45 "Groebner_Examples",
46 "MT",
47 "Unification",
48 "Primrec",
49 "Tarski",
50 "Classical",
51 "Set_Theory",
52 "Meson_Test",
53 "Termination",
54 "Coherent",
55 "PresburgerEx",
56 "ReflectionEx",
57 "Sqrt",
58 "Sqrt_Script",
59 "Transfer_Ex",
60 "Transfer_Int_Nat",
61 "HarmonicSeries",
62 "Refute_Examples",
63 "Landau",
64 "Execute_Choice",
65 "Summation",
66 "Gauge_Integration",
67 "Dedekind_Real",
68 "Quicksort",
69 "Birthday_Paradox",
70 "List_to_Set_Comprehension_Examples",
71 "Seq",
72 "Simproc_Tests",
73 "Executable_Relation"
74 ];
76 use_thy "SVC_Oracle";
77 if getenv "SVC_HOME" = "" then ()
78 else use_thy "svc_test";
80 (*requires zChaff (or some other reasonably fast SAT solver)*)
81 if getenv "ZCHAFF_HOME" = "" then ()
82 else use_thy "Sudoku";
84 (*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
85 (*global side-effects ahead!*)
86 try use_thy "SAT_Examples"; (* FIXME try!? (not really a proper test) *)