| author | bulwahn |
| Tue, 07 Jun 2011 11:24:16 +0200 | |
| changeset 44083 | 3c58977e0911 |
| parent 44079 | 04c886a1d1a5 |
| parent 44064 | c9e87dc92d9e |
| child 44668 | eb9be23db2b7 |
| 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 "Efficient_Nat_examples",
9 "~~/src/HOL/Library/FuncSet",
10 "Eval_Examples",
11 "Normalization_by_Evaluation",
12 "Hebrew",
13 "Chinese",
14 "Serbian",
15 "ATP_Export"
16 ];
18 use_thys [
19 "Iff_Oracle",
20 "Coercion_Examples",
21 "Numeral",
22 "Higher_Order_Logic",
23 "Abstract_NAT",
24 "Guess",
25 "Binary",
26 "Recdefs",
27 "Fundefs",
28 "Induction_Schema",
29 "InductiveInvariant_examples",
30 "LocaleTest2",
31 "Records",
32 "While_Combinator_Example",
33 "MonoidGroup",
34 "BinEx",
35 "Hex_Bin_Examples",
36 "Antiquote",
37 "Multiquote",
38 "PER",
39 "NatSum",
40 "ThreeDivides",
41 "Intuitionistic",
42 "CTL",
43 "Arith_Examples",
44 "BT",
45 "Tree23",
46 "MergeSort",
47 "Lagrange",
48 "Groebner_Examples",
49 "MT",
50 "Unification",
51 "Primrec",
52 "Tarski",
53 "Classical",
54 "set",
55 "Meson_Test",
56 "Termination",
57 "Coherent",
58 "PresburgerEx",
59 "ReflectionEx",
60 "BinEx",
61 "Sqrt",
62 "Sqrt_Script",
63 "Transfer_Ex",
64 "Arithmetic_Series_Complex",
65 "HarmonicSeries",
66 "Refute_Examples",
67 "Quickcheck_Examples",
68 "SML_Quickcheck_Examples",
69 "Quickcheck_Lattice_Examples",
70 "Landau",
71 "Execute_Choice",
72 "Summation",
73 "Gauge_Integration",
74 "Dedekind_Real",
75 "Quicksort",
76 "Birthday_Paradox",
77 "List_to_Set_Comprehension_Examples",
78 "Set_Algebras"
79 ];
81 Unsynchronized.setmp Proofterm.proofs (! Proofterm.proofs)
82 use_thy "CASC_Setup";
84 if getenv "ISABELLE_GHC" = "" then ()
85 else use_thy "Quickcheck_Narrowing_Examples";
87 use_thy "SVC_Oracle";
88 if getenv "SVC_HOME" = "" then ()
89 else use_thy "svc_test";
91 (*requires zChaff (or some other reasonably fast SAT solver)*)
92 if getenv "ZCHAFF_HOME" = "" then ()
93 else use_thy "Sudoku";
95 (*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
96 (*global side-effects ahead!*)
97 try use_thy "SAT_Examples"; (* FIXME try!? (not really a proper test) *)