| author | huffman |
| Mon, 10 May 2010 11:30:05 -0700 | |
| changeset 36787 | 27da0a27b76f |
| parent 35952 | 0460ff79bb52 |
| child 36955 | 5fb251d1c32f |
| 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 ];
17 use_thys [
18 "Numeral",
19 "Higher_Order_Logic",
20 "Abstract_NAT",
21 "Guess",
22 "Binary",
23 "Recdefs",
24 "Fundefs",
25 "Induction_Schema",
26 "InductiveInvariant_examples",
27 "LocaleTest2",
28 "Records",
29 "MonoidGroup",
30 "BinEx",
31 "Hex_Bin_Examples",
32 "Antiquote",
33 "Multiquote",
34 "PER",
35 "NatSum",
36 "ThreeDivides",
37 "Intuitionistic",
38 "CTL",
39 "Arith_Examples",
40 "BT",
41 "Tree23",
42 "MergeSort",
43 "Lagrange",
44 "Groebner_Examples",
45 "MT",
46 "Unification",
47 "Primrec",
48 "Tarski",
49 "Adder",
50 "Classical",
51 "set",
52 "Meson_Test",
53 "Termination",
54 "Coherent",
55 "PresburgerEx",
56 "ReflectionEx",
57 "BinEx",
58 "Sqrt",
59 "Sqrt_Script",
60 "Transfer_Ex",
61 "Arithmetic_Series_Complex",
62 "HarmonicSeries",
63 "Refute_Examples",
64 "Quickcheck_Examples",
65 "Landau",
66 "Execute_Choice",
67 "Summation",
68 "Gauge_Integration",
69 "Dedekind_Real"
70 ];
72 HTML.with_charset "utf-8" (no_document use_thys)
73 ["Hebrew", "Chinese", "Serbian"];
75 (setmp_noncritical proofs 2 (setmp_noncritical Goal.parallel_proofs 0 use_thy))
76 "Hilbert_Classical";
78 use_thy "SVC_Oracle";
79 if getenv "SVC_HOME" = "" then ()
80 else use_thy "svc_test";
82 (*requires zChaff (or some other reasonably fast SAT solver)*)
83 if getenv "ZCHAFF_HOME" = "" then ()
84 else use_thy "Sudoku";
86 (*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
87 (*global side-effects ahead!*)
88 try use_thy "SAT_Examples"; (* FIXME try!? (not really a proper test) *)