| author | bulwahn |
| Thu, 12 Nov 2009 20:39:02 +0100 | |
| changeset 33651 | e4aad90618ad |
| parent 33546 | 5e2d381b0695 |
| child 35160 | 6eb2b6c1d2d5 |
| permissions | -rw-r--r-- |
1 (* Title: HOL/ex/ROOT.ML
3 Miscellaneous examples for Higher-Order Logic.
4 *)
6 no_document use_thys [
7 "State_Monad",
8 "Efficient_Nat_examples",
9 "FuncSet",
10 "Word",
11 "Eval_Examples",
12 "Codegenerator_Test",
13 "Codegenerator_Pretty_Test",
14 "NormalForm",
15 "Predicate_Compile",
16 "Predicate_Compile_ex",
17 "Predicate_Compile_Quickcheck"
18 ];
20 use_thys [
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 "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 "Adder",
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 "Landau"
69 ];
71 HTML.with_charset "utf-8" (no_document use_thys)
72 ["Hebrew", "Chinese", "Serbian"];
74 (setmp_noncritical proofs 2 (setmp_noncritical Goal.parallel_proofs 0 use_thy))
75 "Hilbert_Classical";
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) *)