author | bulwahn |
Wed, 30 Mar 2011 10:31:02 +0200 | |
changeset 43032 | d1b39536e1fb |
parent 42949 | d5bf0ce40bd7 |
child 43472 | cddab94eeb14 |
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 ];
17 use_thys [
18 "Iff_Oracle",
19 "Coercion_Examples",
20 "Numeral",
21 "Higher_Order_Logic",
22 "Abstract_NAT",
23 "Guess",
24 "Binary",
25 "Recdefs",
26 "Fundefs",
27 "Induction_Schema",
28 "InductiveInvariant_examples",
29 "LocaleTest2",
30 "Records",
31 "While_Combinator_Example",
32 "MonoidGroup",
33 "BinEx",
34 "Hex_Bin_Examples",
35 "Antiquote",
36 "Multiquote",
37 "PER",
38 "NatSum",
39 "ThreeDivides",
40 "Intuitionistic",
41 "CTL",
42 "Arith_Examples",
43 "BT",
44 "Tree23",
45 "MergeSort",
46 "Lagrange",
47 "Groebner_Examples",
48 "MT",
49 "Unification",
50 "Primrec",
51 "Tarski",
52 "Classical",
53 "set",
54 "Meson_Test",
55 "Termination",
56 "Coherent",
57 "PresburgerEx",
58 "ReflectionEx",
59 "BinEx",
60 "Sqrt",
61 "Sqrt_Script",
62 "Transfer_Ex",
63 "Arithmetic_Series_Complex",
64 "HarmonicSeries",
65 "Refute_Examples",
66 "Quickcheck_Examples",
67 "SML_Quickcheck_Examples",
68 "Quickcheck_Lattice_Examples",
69 "Landau",
70 "Execute_Choice",
71 "Summation",
72 "Gauge_Integration",
73 "Dedekind_Real",
74 "Quicksort",
75 "Birthday_Paradoxon",
76 "List_to_Set_Comprehension_Examples",
77 "Set_Algebras"
78 ];
80 Unsynchronized.setmp Proofterm.proofs (! Proofterm.proofs)
81 use_thy "TPTP";
83 if getenv "ISABELLE_GHC" = "" then ()
84 else use_thy "Quickcheck_Narrowing_Examples";
86 use_thy "SVC_Oracle";
87 if getenv "SVC_HOME" = "" then ()
88 else use_thy "svc_test";
90 (*requires zChaff (or some other reasonably fast SAT solver)*)
91 if getenv "ZCHAFF_HOME" = "" then ()
92 else use_thy "Sudoku";
94 (*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
95 (*global side-effects ahead!*)
96 try use_thy "SAT_Examples"; (* FIXME try!? (not really a proper test) *)