|
wenzelm@12115
|
1 |
(* Title: HOL/ex/ROOT.ML
|
|
wenzelm@11586
|
2 |
|
|
wenzelm@12115
|
3 |
Miscellaneous examples for Higher-Order Logic.
|
|
wenzelm@12115
|
4 |
*)
|
|
wenzelm@12115
|
5 |
|
|
wenzelm@24528
|
6 |
no_document use_thys [
|
|
wenzelm@24740
|
7 |
"State_Monad",
|
|
haftmann@25963
|
8 |
"Efficient_Nat_examples",
|
|
haftmann@25963
|
9 |
"FuncSet",
|
|
haftmann@25963
|
10 |
"Word",
|
|
haftmann@25963
|
11 |
"Eval_Examples",
|
|
haftmann@31378
|
12 |
"Codegenerator_Test",
|
|
haftmann@31378
|
13 |
"Codegenerator_Pretty_Test",
|
|
bulwahn@35952
|
14 |
"NormalForm"
|
|
haftmann@25963
|
15 |
];
|
|
haftmann@25963
|
16 |
|
|
wenzelm@24478
|
17 |
use_thys [
|
|
haftmann@28021
|
18 |
"Numeral",
|
|
wenzelm@24478
|
19 |
"Higher_Order_Logic",
|
|
wenzelm@24478
|
20 |
"Abstract_NAT",
|
|
wenzelm@24478
|
21 |
"Guess",
|
|
wenzelm@24478
|
22 |
"Binary",
|
|
wenzelm@24478
|
23 |
"Recdefs",
|
|
wenzelm@24478
|
24 |
"Fundefs",
|
|
krauss@33471
|
25 |
"Induction_Schema",
|
|
wenzelm@24478
|
26 |
"InductiveInvariant_examples",
|
|
wenzelm@24478
|
27 |
"LocaleTest2",
|
|
wenzelm@24478
|
28 |
"Records",
|
|
wenzelm@24478
|
29 |
"MonoidGroup",
|
|
wenzelm@24478
|
30 |
"BinEx",
|
|
wenzelm@24478
|
31 |
"Hex_Bin_Examples",
|
|
wenzelm@24478
|
32 |
"Antiquote",
|
|
wenzelm@24478
|
33 |
"Multiquote",
|
|
wenzelm@24478
|
34 |
"PER",
|
|
wenzelm@24478
|
35 |
"NatSum",
|
|
wenzelm@24478
|
36 |
"ThreeDivides",
|
|
wenzelm@24478
|
37 |
"Intuitionistic",
|
|
wenzelm@24478
|
38 |
"CTL",
|
|
wenzelm@24478
|
39 |
"Arith_Examples",
|
|
wenzelm@24478
|
40 |
"BT",
|
|
nipkow@33425
|
41 |
"Tree23",
|
|
wenzelm@24478
|
42 |
"MergeSort",
|
|
wenzelm@24478
|
43 |
"Lagrange",
|
|
wenzelm@24478
|
44 |
"Groebner_Examples",
|
|
wenzelm@24478
|
45 |
"MT",
|
|
wenzelm@24478
|
46 |
"Unification",
|
|
wenzelm@24740
|
47 |
"Primrec",
|
|
wenzelm@24740
|
48 |
"Tarski",
|
|
wenzelm@25738
|
49 |
"Adder",
|
|
wenzelm@25738
|
50 |
"Classical",
|
|
wenzelm@25738
|
51 |
"set",
|
|
haftmann@27436
|
52 |
"Meson_Test",
|
|
krauss@29181
|
53 |
"Termination",
|
|
wenzelm@29376
|
54 |
"Coherent",
|
|
wenzelm@29376
|
55 |
"PresburgerEx",
|
|
wenzelm@29377
|
56 |
"ReflectionEx",
|
|
wenzelm@29377
|
57 |
"BinEx",
|
|
wenzelm@29377
|
58 |
"Sqrt",
|
|
wenzelm@29377
|
59 |
"Sqrt_Script",
|
|
haftmann@32560
|
60 |
"Transfer_Ex",
|
|
wenzelm@29377
|
61 |
"Arithmetic_Series_Complex",
|
|
wenzelm@29377
|
62 |
"HarmonicSeries",
|
|
wenzelm@29377
|
63 |
"Refute_Examples",
|
|
chaieb@29697
|
64 |
"Quickcheck_Examples",
|
|
haftmann@35160
|
65 |
"Landau",
|
|
haftmann@35163
|
66 |
"Execute_Choice",
|
|
hoelzl@35328
|
67 |
"Summation",
|
|
huffman@36787
|
68 |
"Gauge_Integration",
|
|
huffman@36787
|
69 |
"Dedekind_Real"
|
|
wenzelm@24478
|
70 |
];
|
|
wenzelm@21256
|
71 |
|
|
wenzelm@33546
|
72 |
HTML.with_charset "utf-8" (no_document use_thys)
|
|
wenzelm@33546
|
73 |
["Hebrew", "Chinese", "Serbian"];
|
|
wenzelm@33546
|
74 |
|
|
wenzelm@32615
|
75 |
(setmp_noncritical proofs 2 (setmp_noncritical Goal.parallel_proofs 0 use_thy))
|
|
wenzelm@32260
|
76 |
"Hilbert_Classical";
|
|
wenzelm@24478
|
77 |
|
|
wenzelm@32428
|
78 |
use_thy "SVC_Oracle";
|
|
wenzelm@32428
|
79 |
if getenv "SVC_HOME" = "" then ()
|
|
wenzelm@32428
|
80 |
else use_thy "svc_test";
|
|
wenzelm@12115
|
81 |
|
|
wenzelm@32428
|
82 |
(*requires zChaff (or some other reasonably fast SAT solver)*)
|
|
wenzelm@32428
|
83 |
if getenv "ZCHAFF_HOME" = "" then ()
|
|
wenzelm@32428
|
84 |
else use_thy "Sudoku";
|
|
webertj@18408
|
85 |
|
|
wenzelm@33546
|
86 |
(*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
|
|
wenzelm@33546
|
87 |
(*global side-effects ahead!*)
|
|
wenzelm@33546
|
88 |
try use_thy "SAT_Examples"; (* FIXME try!? (not really a proper test) *)
|