| author | wenzelm |
| Sat, 28 Feb 2009 21:34:33 +0100 | |
| changeset 30179 | c703c9368c12 |
| parent 29745 | b8b9d529663b |
| child 30374 | 7311a1546d85 |
| 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 "ExecutableContent",
10 "FuncSet",
11 "Word",
12 "Eval_Examples",
13 "Quickcheck_Generators",
14 "Term_Of_Syntax",
15 "Codegenerator",
16 "Codegenerator_Pretty",
17 "NormalForm",
18 "../NumberTheory/Factorization"
19 ];
21 use_thys [
22 "Numeral",
23 "ImperativeQuicksort",
24 "Higher_Order_Logic",
25 "Abstract_NAT",
26 "Guess",
27 "Binary",
28 "Recdefs",
29 "Fundefs",
30 "Induction_Scheme",
31 "InductiveInvariant_examples",
32 "LocaleTest2",
33 "Records",
34 "MonoidGroup",
35 "BinEx",
36 "Hex_Bin_Examples",
37 "Antiquote",
38 "Multiquote",
39 "PER",
40 "NatSum",
41 "ThreeDivides",
42 "Intuitionistic",
43 "CTL",
44 "Arith_Examples",
45 "BT",
46 "MergeSort",
47 "Lagrange",
48 "Groebner_Examples",
49 "MT",
50 "Unification",
51 "Commutative_RingEx",
52 "Commutative_Ring_Complete",
53 "Primrec",
54 "Tarski",
55 "Adder",
56 "Classical",
57 "set",
58 "Meson_Test",
59 "Code_Antiq",
60 "Termination",
61 "Coherent",
62 "Dense_Linear_Order_Ex",
63 "PresburgerEx",
64 "ReflectionEx",
65 "BinEx",
66 "Sqrt",
67 "Sqrt_Script",
68 "Arithmetic_Series_Complex",
69 "HarmonicSeries",
70 "Refute_Examples",
71 "Quickcheck_Examples",
72 "Formal_Power_Series_Examples"
73 ];
75 setmp Proofterm.proofs 2 use_thy "Hilbert_Classical";
78 use_thy "SVC_Oracle";
80 fun svc_enabled () = getenv "SVC_HOME" <> "";
81 fun if_svc_enabled f x = if svc_enabled () then f x else ();
83 if_svc_enabled use_thy "svc_test";
86 (* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)
87 (* installed: *)
88 try use_thy "SAT_Examples";
90 (* requires zChaff (or some other reasonably fast SAT solver) to be *)
91 (* installed: *)
92 if getenv "ZCHAFF_HOME" <> "" then
93 use_thy "Sudoku"
94 else ();
96 HTML.with_charset "utf-8" (no_document use_thys)
97 ["Hebrew", "Chinese", "Serbian"];