| author | Andreas Lochbihler |
| Tue, 29 May 2012 15:31:58 +0200 | |
| changeset 49043 | a5377f6d9f14 |
| parent 48524 | f7df7104d13e |
| child 49056 | d60f6b41bf2d |
| 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 "~~/src/HOL/Library/FinFun"
16 ];
18 use_thys [
19 "Iff_Oracle",
20 "Coercion_Examples",
21 "Numeral_Representation",
22 "Higher_Order_Logic",
23 "Abstract_NAT",
24 "Guess",
25 "Binary",
26 "Fundefs",
27 "Induction_Schema",
28 "LocaleTest2",
29 "Records",
30 "While_Combinator_Example",
31 "MonoidGroup",
32 "BinEx",
33 "Hex_Bin_Examples",
34 "Antiquote",
35 "Multiquote",
36 "PER",
37 "NatSum",
38 "ThreeDivides",
39 "Intuitionistic",
40 "CTL",
41 "Arith_Examples",
42 "BT",
43 "Tree23",
44 "MergeSort",
45 "Lagrange",
46 "Groebner_Examples",
47 "MT",
48 "Unification",
49 "Primrec",
50 "Tarski",
51 "Classical",
52 "Set_Theory",
53 "Meson_Test",
54 "Termination",
55 "Coherent",
56 "PresburgerEx",
57 "ReflectionEx",
58 "Sqrt",
59 "Sqrt_Script",
60 "Transfer_Ex",
61 "Transfer_Int_Nat",
62 "HarmonicSeries",
63 "Refute_Examples",
64 "Landau",
65 "Execute_Choice",
66 "Summation",
67 "Gauge_Integration",
68 "Dedekind_Real",
69 "Quicksort",
70 "Birthday_Paradox",
71 "List_to_Set_Comprehension_Examples",
72 "Seq",
73 "Simproc_Tests",
74 "Executable_Relation",
75 "FinFunPred"
76 ];
78 use_thy "SVC_Oracle";
79 if getenv "SVC_HOME" = "" then ()
80 else use_thy "svc_test";
82 (*requires zChaff (or some other reasonably fast SAT solver)*)
83 if getenv "ZCHAFF_HOME" = "" then ()
84 else use_thy "Sudoku";
86 (*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
87 (*global side-effects ahead!*)
88 try use_thy "SAT_Examples"; (* FIXME try!? (not really a proper test) *)