author | haftmann |
Wed, 17 Feb 2010 09:48:53 +0100 | |
changeset 35160 | 6eb2b6c1d2d5 |
parent 33651 | e4aad90618ad |
child 35163 | 2e0966d6f951 |
permissions | -rw-r--r-- |
12115 | 1 |
(* Title: HOL/ex/ROOT.ML |
11586 | 2 |
|
12115 | 3 |
Miscellaneous examples for Higher-Order Logic. |
4 |
*) |
|
5 |
||
24528 | 6 |
no_document use_thys [ |
24740 | 7 |
"State_Monad", |
25963 | 8 |
"Efficient_Nat_examples", |
9 |
"FuncSet", |
|
10 |
"Word", |
|
11 |
"Eval_Examples", |
|
31378 | 12 |
"Codegenerator_Test", |
13 |
"Codegenerator_Pretty_Test", |
|
29377 | 14 |
"NormalForm", |
31129
d2cead76fca2
split Predicate_Compile examples into separate theory
haftmann
parents:
30740
diff
changeset
|
15 |
"Predicate_Compile", |
33651
e4aad90618ad
adding the predicate compiler quickcheck to the ex/ROOT.ML; adopting this quickcheck to the latest changes
bulwahn
parents:
33546
diff
changeset
|
16 |
"Predicate_Compile_ex", |
e4aad90618ad
adding the predicate compiler quickcheck to the ex/ROOT.ML; adopting this quickcheck to the latest changes
bulwahn
parents:
33546
diff
changeset
|
17 |
"Predicate_Compile_Quickcheck" |
25963 | 18 |
]; |
19 |
||
24478 | 20 |
use_thys [ |
28021 | 21 |
"Numeral", |
24478 | 22 |
"Higher_Order_Logic", |
23 |
"Abstract_NAT", |
|
24 |
"Guess", |
|
25 |
"Binary", |
|
26 |
"Recdefs", |
|
27 |
"Fundefs", |
|
33471 | 28 |
"Induction_Schema", |
24478 | 29 |
"InductiveInvariant_examples", |
30 |
"LocaleTest2", |
|
31 |
"Records", |
|
32 |
"MonoidGroup", |
|
33 |
"BinEx", |
|
34 |
"Hex_Bin_Examples", |
|
35 |
"Antiquote", |
|
36 |
"Multiquote", |
|
37 |
"PER", |
|
38 |
"NatSum", |
|
39 |
"ThreeDivides", |
|
40 |
"Intuitionistic", |
|
41 |
"CTL", |
|
42 |
"Arith_Examples", |
|
43 |
"BT", |
|
33436 | 44 |
"Tree23", |
24478 | 45 |
"MergeSort", |
46 |
"Lagrange", |
|
47 |
"Groebner_Examples", |
|
48 |
"MT", |
|
49 |
"Unification", |
|
24740 | 50 |
"Primrec", |
51 |
"Tarski", |
|
25738
b091cbae3e2a
included meson/metis tests in simultaneous use_thys;
wenzelm
parents:
25568
diff
changeset
|
52 |
"Adder", |
b091cbae3e2a
included meson/metis tests in simultaneous use_thys;
wenzelm
parents:
25568
diff
changeset
|
53 |
"Classical", |
b091cbae3e2a
included meson/metis tests in simultaneous use_thys;
wenzelm
parents:
25568
diff
changeset
|
54 |
"set", |
27436 | 55 |
"Meson_Test", |
29181
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
28952
diff
changeset
|
56 |
"Termination", |
29376 | 57 |
"Coherent", |
58 |
"PresburgerEx", |
|
29377 | 59 |
"ReflectionEx", |
60 |
"BinEx", |
|
61 |
"Sqrt", |
|
62 |
"Sqrt_Script", |
|
32560 | 63 |
"Transfer_Ex", |
29377 | 64 |
"Arithmetic_Series_Complex", |
65 |
"HarmonicSeries", |
|
66 |
"Refute_Examples", |
|
29697
e8785144719d
Added Formal_Power_Series_Examples to HOL-ex image
chaieb
parents:
29650
diff
changeset
|
67 |
"Quickcheck_Examples", |
35160
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
33651
diff
changeset
|
68 |
"Landau", |
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
33651
diff
changeset
|
69 |
"Execute_Choice" |
24478 | 70 |
]; |
21256 | 71 |
|
33546
5e2d381b0695
try SAT_Examples last, to minimize impact of global side-effects;
wenzelm
parents:
33471
diff
changeset
|
72 |
HTML.with_charset "utf-8" (no_document use_thys) |
5e2d381b0695
try SAT_Examples last, to minimize impact of global side-effects;
wenzelm
parents:
33471
diff
changeset
|
73 |
["Hebrew", "Chinese", "Serbian"]; |
5e2d381b0695
try SAT_Examples last, to minimize impact of global side-effects;
wenzelm
parents:
33471
diff
changeset
|
74 |
|
32615
20f1edc87b7d
Hilbert_Classical: more precise control of parallel_proofs;
wenzelm
parents:
32560
diff
changeset
|
75 |
(setmp_noncritical proofs 2 (setmp_noncritical Goal.parallel_proofs 0 use_thy)) |
32256
8721c74c5382
Hilbert_Classical: sequential loading due to @{prf}, which joins within a critical section (via options);
wenzelm
parents:
32254
diff
changeset
|
76 |
"Hilbert_Classical"; |
24478 | 77 |
|
29376 | 78 |
use_thy "SVC_Oracle"; |
32428
700ed1f4c576
SAT_Examples: removed obsolete Future.shutdown() workaround -- internal exception propagation should now work reliably;
wenzelm
parents:
32259
diff
changeset
|
79 |
if getenv "SVC_HOME" = "" then () |
700ed1f4c576
SAT_Examples: removed obsolete Future.shutdown() workaround -- internal exception propagation should now work reliably;
wenzelm
parents:
32259
diff
changeset
|
80 |
else use_thy "svc_test"; |
29376 | 81 |
|
32428
700ed1f4c576
SAT_Examples: removed obsolete Future.shutdown() workaround -- internal exception propagation should now work reliably;
wenzelm
parents:
32259
diff
changeset
|
82 |
(*requires zChaff (or some other reasonably fast SAT solver)*) |
700ed1f4c576
SAT_Examples: removed obsolete Future.shutdown() workaround -- internal exception propagation should now work reliably;
wenzelm
parents:
32259
diff
changeset
|
83 |
if getenv "ZCHAFF_HOME" = "" then () |
700ed1f4c576
SAT_Examples: removed obsolete Future.shutdown() workaround -- internal exception propagation should now work reliably;
wenzelm
parents:
32259
diff
changeset
|
84 |
else use_thy "Sudoku"; |
18408 | 85 |
|
33546
5e2d381b0695
try SAT_Examples last, to minimize impact of global side-effects;
wenzelm
parents:
33471
diff
changeset
|
86 |
(*requires a proof-generating SAT solver (zChaff or MiniSAT)*) |
5e2d381b0695
try SAT_Examples last, to minimize impact of global side-effects;
wenzelm
parents:
33471
diff
changeset
|
87 |
(*global side-effects ahead!*) |
5e2d381b0695
try SAT_Examples last, to minimize impact of global side-effects;
wenzelm
parents:
33471
diff
changeset
|
88 |
try use_thy "SAT_Examples"; (* FIXME try!? (not really a proper test) *) |