author | huffman |
Sun, 25 Mar 2012 20:15:39 +0200 | |
changeset 47978 | 2a1953f0d20d |
parent 47456 | f462e49eaf11 |
child 48094 | 4fc34c628474 |
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 "Arithmetic_Series_Complex",
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 "Set_Algebras",
72 "Seq",
73 "Simproc_Tests",
74 "Executable_Relation"
75 ];
77 use_thy "SVC_Oracle";
78 if getenv "SVC_HOME" = "" then ()
79 else use_thy "svc_test";
81 (*requires zChaff (or some other reasonably fast SAT solver)*)
82 if getenv "ZCHAFF_HOME" = "" then ()
83 else use_thy "Sudoku";
85 (*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
86 (*global side-effects ahead!*)
87 try use_thy "SAT_Examples"; (* FIXME try!? (not really a proper test) *)