author | haftmann |
Tue, 01 Jul 2008 07:58:17 +0200 | |
changeset 27421 | 7e458bd56860 |
parent 26265 | 4b63b9e9b10d |
child 27436 | 9581777503e9 |
permissions | -rw-r--r-- |
12115 | 1 |
(* Title: HOL/ex/ROOT.ML |
2 |
ID: $Id$ |
|
11586 | 3 |
|
12115 | 4 |
Miscellaneous examples for Higher-Order Logic. |
5 |
*) |
|
6 |
||
24528 | 7 |
no_document use_thys [ |
24478 | 8 |
"Parity", |
24740 | 9 |
"GCD", |
10 |
"Eval", |
|
11 |
"State_Monad", |
|
25963 | 12 |
"Efficient_Nat_examples", |
13 |
"ExecutableContent", |
|
14 |
"FuncSet", |
|
15 |
"Word", |
|
16 |
"Eval_Examples", |
|
26265 | 17 |
"Quickcheck" |
25963 | 18 |
]; |
19 |
||
25975
bcb1e9b7644b
Codegenerator vs. Codegenerator_Pretty: loaded sequentially, due to hazardous ML sections;
wenzelm
parents:
25963
diff
changeset
|
20 |
no_document use_thy "Codegenerator"; |
bcb1e9b7644b
Codegenerator vs. Codegenerator_Pretty: loaded sequentially, due to hazardous ML sections;
wenzelm
parents:
25963
diff
changeset
|
21 |
no_document use_thy "Codegenerator_Pretty"; |
24478 | 22 |
|
23 |
use_thys [ |
|
24 |
"Higher_Order_Logic", |
|
25 |
"Abstract_NAT", |
|
26 |
"Guess", |
|
27 |
"Binary", |
|
28 |
"Recdefs", |
|
29 |
"Fundefs", |
|
25568 | 30 |
"Induction_Scheme", |
24478 | 31 |
"InductiveInvariant_examples", |
32 |
"Locales", |
|
33 |
"LocaleTest2", |
|
34 |
"Records", |
|
35 |
"MonoidGroup", |
|
36 |
"BinEx", |
|
37 |
"Hex_Bin_Examples", |
|
38 |
"Antiquote", |
|
39 |
"Multiquote", |
|
40 |
"PER", |
|
41 |
"NatSum", |
|
42 |
"ThreeDivides", |
|
43 |
"Intuitionistic", |
|
44 |
"CTL", |
|
45 |
"Arith_Examples", |
|
46 |
"BT", |
|
47 |
"MergeSort", |
|
48 |
"Puzzle", |
|
49 |
"Lagrange", |
|
50 |
"Groebner_Examples", |
|
51 |
"MT", |
|
52 |
"Unification", |
|
53 |
"Commutative_RingEx", |
|
24740 | 54 |
"Commutative_Ring_Complete", |
55 |
"Primrec", |
|
56 |
"Tarski", |
|
25738
b091cbae3e2a
included meson/metis tests in simultaneous use_thys;
wenzelm
parents:
25568
diff
changeset
|
57 |
"Adder", |
b091cbae3e2a
included meson/metis tests in simultaneous use_thys;
wenzelm
parents:
25568
diff
changeset
|
58 |
"Classical", |
b091cbae3e2a
included meson/metis tests in simultaneous use_thys;
wenzelm
parents:
25568
diff
changeset
|
59 |
"set", |
b091cbae3e2a
included meson/metis tests in simultaneous use_thys;
wenzelm
parents:
25568
diff
changeset
|
60 |
"Meson_Test" |
24478 | 61 |
]; |
21256 | 62 |
|
25374 | 63 |
setmp Proofterm.proofs 2 time_use_thy "Hilbert_Classical"; |
24478 | 64 |
|
23454
c54975167be9
replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
wenzelm
parents:
23302
diff
changeset
|
65 |
time_use_thy "Dense_Linear_Order_Ex"; |
13880 | 66 |
time_use_thy "PresburgerEx"; |
23808 | 67 |
time_use_thy "Reflected_Presburger"; |
12115 | 68 |
|
20325 | 69 |
time_use_thy "Reflection"; |
12115 | 70 |
|
12869 | 71 |
time_use_thy "SVC_Oracle"; |
12115 | 72 |
if_svc_enabled time_use_thy "svc_test"; |
14459 | 73 |
|
23191 | 74 |
(* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *) |
75 |
(* installed: *) |
|
18678 | 76 |
try time_use_thy "SAT_Examples"; |
17618
1330157e156a
new sat tactic imports resolution proofs from zChaff
webertj
parents:
17505
diff
changeset
|
77 |
|
23191 | 78 |
(* requires zChaff (or some other reasonably fast SAT solver) to be *) |
79 |
(* installed: *) |
|
18408 | 80 |
if getenv "ZCHAFF_HOME" <> "" then |
81 |
time_use_thy "Sudoku" |
|
23191 | 82 |
else (); |
18408 | 83 |
|
14462 | 84 |
time_use_thy "Refute_Examples"; |
14592
dd1a2905ea73
Added theory with examples for quickcheck command.
berghofe
parents:
14569
diff
changeset
|
85 |
time_use_thy "Quickcheck_Examples"; |
19832 | 86 |
no_document time_use_thy "NormalForm"; |
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
14482
diff
changeset
|
87 |
|
25975
bcb1e9b7644b
Codegenerator vs. Codegenerator_Pretty: loaded sequentially, due to hazardous ML sections;
wenzelm
parents:
25963
diff
changeset
|
88 |
HTML.with_charset "utf-8" (no_document use_thys) ["Hebrew", "Chinese"]; |
bcb1e9b7644b
Codegenerator vs. Codegenerator_Pretty: loaded sequentially, due to hazardous ML sections;
wenzelm
parents:
25963
diff
changeset
|
89 |
|
27421 | 90 |
no_document use_thys [ |
91 |
"../NumberTheory/Factorization", |
|
92 |
"../Library/BigO", |
|
93 |
"../Library/NatPair" |
|
94 |
]; |
|
95 |
||
96 |
use_thys [ |
|
97 |
"../Complex/ex/BinEx", |
|
98 |
"../Complex/ex/Sqrt", |
|
99 |
"../Complex/ex/Sqrt_Script", |
|
100 |
"../Complex/ex/NSPrimes", |
|
101 |
"../Complex/ex/BigO_Complex", |
|
102 |
||
103 |
"../Complex/ex/Arithmetic_Series_Complex", |
|
104 |
"../Complex/ex/HarmonicSeries", |
|
105 |
||
106 |
"../Complex/ex/DenumRat", |
|
107 |
||
108 |
"../Complex/ex/MIR", |
|
109 |
"../Complex/ex/ReflectedFerrack" |
|
110 |
]; |
|
111 |