| author | krauss |
| Fri, 09 Jul 2010 17:15:03 +0200 | |
| changeset 37759 | 8380686be5cd |
| parent 37686 | 71e84a203c19 |
| child 38157 | 67ccea8a4761 |
| 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 "NormalForm"
12 ];
14 use_thys [
15 "Numeral",
16 "Higher_Order_Logic",
17 "Abstract_NAT",
18 "Guess",
19 "Binary",
20 "Recdefs",
21 "Fundefs",
22 "Induction_Schema",
23 "InductiveInvariant_examples",
24 "LocaleTest2",
25 "Records",
26 "While_Combinator_Example",
27 "MonoidGroup",
28 "BinEx",
29 "Hex_Bin_Examples",
30 "Antiquote",
31 "Multiquote",
32 "PER",
33 "NatSum",
34 "ThreeDivides",
35 "Intuitionistic",
36 "CTL",
37 "Arith_Examples",
38 "BT",
39 "Tree23",
40 "MergeSort",
41 "Lagrange",
42 "Groebner_Examples",
43 "MT",
44 "Unification",
45 "Primrec",
46 "Tarski",
47 "Classical",
48 "set",
49 "Meson_Test",
50 "Termination",
51 "Coherent",
52 "PresburgerEx",
53 "ReflectionEx",
54 "BinEx",
55 "Sqrt",
56 "Sqrt_Script",
57 "Transfer_Ex",
58 "Arithmetic_Series_Complex",
59 "HarmonicSeries",
60 "Refute_Examples",
61 "Quickcheck_Examples",
62 "Landau",
63 "Execute_Choice",
64 "Summation",
65 "Gauge_Integration",
66 "Dedekind_Real"
67 ];
69 HTML.with_charset "utf-8" (no_document use_thys)
70 ["Hebrew", "Chinese", "Serbian"];
72 (setmp_noncritical proofs 2 (setmp_noncritical Multithreading.max_threads 1 use_thy))
73 "Hilbert_Classical";
75 use_thy "SVC_Oracle";
76 if getenv "SVC_HOME" = "" then ()
77 else use_thy "svc_test";
79 (*requires zChaff (or some other reasonably fast SAT solver)*)
80 if getenv "ZCHAFF_HOME" = "" then ()
81 else use_thy "Sudoku";
83 (*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
84 (*global side-effects ahead!*)
85 try use_thy "SAT_Examples"; (* FIXME try!? (not really a proper test) *)