| author | wenzelm |
| Wed, 02 Jun 2010 13:18:21 +0200 | |
| changeset 37280 | 0fb011773adc |
| parent 36955 | 5fb251d1c32f |
| child 37686 | 71e84a203c19 |
| 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 "Eval_Examples",
11 "Codegenerator_Test",
12 "Codegenerator_Pretty_Test",
13 "NormalForm"
14 ];
16 use_thys [
17 "Numeral",
18 "Higher_Order_Logic",
19 "Abstract_NAT",
20 "Guess",
21 "Binary",
22 "Recdefs",
23 "Fundefs",
24 "Induction_Schema",
25 "InductiveInvariant_examples",
26 "LocaleTest2",
27 "Records",
28 "MonoidGroup",
29 "BinEx",
30 "Hex_Bin_Examples",
31 "Antiquote",
32 "Multiquote",
33 "PER",
34 "NatSum",
35 "ThreeDivides",
36 "Intuitionistic",
37 "CTL",
38 "Arith_Examples",
39 "BT",
40 "Tree23",
41 "MergeSort",
42 "Lagrange",
43 "Groebner_Examples",
44 "MT",
45 "Unification",
46 "Primrec",
47 "Tarski",
48 "Classical",
49 "set",
50 "Meson_Test",
51 "Termination",
52 "Coherent",
53 "PresburgerEx",
54 "ReflectionEx",
55 "BinEx",
56 "Sqrt",
57 "Sqrt_Script",
58 "Transfer_Ex",
59 "Arithmetic_Series_Complex",
60 "HarmonicSeries",
61 "Refute_Examples",
62 "Quickcheck_Examples",
63 "Landau",
64 "Execute_Choice",
65 "Summation",
66 "Gauge_Integration",
67 "Dedekind_Real"
68 ];
70 HTML.with_charset "utf-8" (no_document use_thys)
71 ["Hebrew", "Chinese", "Serbian"];
73 (setmp_noncritical proofs 2 (setmp_noncritical Multithreading.max_threads 1 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) *)