| author | wenzelm |
| Tue, 10 Nov 2009 13:17:50 +0100 | |
| changeset 33546 | 5e2d381b0695 |
| parent 33471 | 5aef13872723 |
| child 33651 | e4aad90618ad |
| 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 ];
19 use_thys [
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 "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 "Adder",
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 "Landau"
68 ];
70 HTML.with_charset "utf-8" (no_document use_thys)
71 ["Hebrew", "Chinese", "Serbian"];
73 (setmp_noncritical proofs 2 (setmp_noncritical Goal.parallel_proofs 0 use_thy))
74 "Hilbert_Classical";
76 use_thy "SVC_Oracle";
77 if getenv "SVC_HOME" = "" then ()
78 else use_thy "svc_test";
80 (*requires zChaff (or some other reasonably fast SAT solver)*)
81 if getenv "ZCHAFF_HOME" = "" then ()
82 else use_thy "Sudoku";
84 (*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
85 (*global side-effects ahead!*)
86 try use_thy "SAT_Examples"; (* FIXME try!? (not really a proper test) *)