| author | haftmann |
| Sun, 22 Jul 2012 09:56:34 +0200 | |
| changeset 49442 | 571cb1df0768 |
| parent 49064 | d862b0d56c49 |
| 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_Syntax"
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 "Set_Comprehension_Pointfree_Tests",
77 "Parallel_Example"
78 ];
80 use_thy "SVC_Oracle";
81 if getenv "SVC_HOME" = "" then ()
82 else use_thy "svc_test";
84 (*requires zChaff (or some other reasonably fast SAT solver)*)
85 if getenv "ZCHAFF_HOME" = "" then ()
86 else use_thy "Sudoku";
88 (*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
89 (*global side-effects ahead!*)
90 try use_thy "SAT_Examples"; (* FIXME try!? (not really a proper test) *)