author | huffman |
Mon, 16 Feb 2009 13:08:21 -0800 | |
changeset 29943 | 922b931fd2eb |
parent 29808 | b8b9d529663b |
child 30179 | c703c9368c12 |
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 |
"ExecutableContent", |
|
10 |
"FuncSet", |
|
11 |
"Word", |
|
12 |
"Eval_Examples", |
|
29808
b8b9d529663b
split of already properly working part of Quickcheck infrastructure
haftmann
parents:
29788
diff
changeset
|
13 |
"Quickcheck_Generators", |
29376 | 14 |
"Term_Of_Syntax", |
15 |
"Codegenerator", |
|
16 |
"Codegenerator_Pretty", |
|
29377 | 17 |
"NormalForm", |
29788 | 18 |
"../NumberTheory/Factorization" |
25963 | 19 |
]; |
20 |
||
24478 | 21 |
use_thys [ |
28021 | 22 |
"Numeral", |
27679 | 23 |
"ImperativeQuicksort", |
24478 | 24 |
"Higher_Order_Logic", |
25 |
"Abstract_NAT", |
|
26 |
"Guess", |
|
27 |
"Binary", |
|
28 |
"Recdefs", |
|
29 |
"Fundefs", |
|
25568 | 30 |
"Induction_Scheme", |
24478 | 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", |
|
24740 | 52 |
"Commutative_Ring_Complete", |
53 |
"Primrec", |
|
54 |
"Tarski", |
|
25738
b091cbae3e2a
included meson/metis tests in simultaneous use_thys;
wenzelm
parents:
25568
diff
changeset
|
55 |
"Adder", |
b091cbae3e2a
included meson/metis tests in simultaneous use_thys;
wenzelm
parents:
25568
diff
changeset
|
56 |
"Classical", |
b091cbae3e2a
included meson/metis tests in simultaneous use_thys;
wenzelm
parents:
25568
diff
changeset
|
57 |
"set", |
27436 | 58 |
"Meson_Test", |
27742 | 59 |
"Code_Antiq", |
29181
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
28952
diff
changeset
|
60 |
"Termination", |
29376 | 61 |
"Coherent", |
62 |
"Dense_Linear_Order_Ex", |
|
63 |
"PresburgerEx", |
|
29377 | 64 |
"ReflectionEx", |
65 |
"BinEx", |
|
66 |
"Sqrt", |
|
67 |
"Sqrt_Script", |
|
68 |
"Arithmetic_Series_Complex", |
|
69 |
"HarmonicSeries", |
|
70 |
"Refute_Examples", |
|
29697
e8785144719d
Added Formal_Power_Series_Examples to HOL-ex image
chaieb
parents:
29650
diff
changeset
|
71 |
"Quickcheck_Examples", |
e8785144719d
Added Formal_Power_Series_Examples to HOL-ex image
chaieb
parents:
29650
diff
changeset
|
72 |
"Formal_Power_Series_Examples" |
24478 | 73 |
]; |
21256 | 74 |
|
29376 | 75 |
setmp Proofterm.proofs 2 use_thy "Hilbert_Classical"; |
24478 | 76 |
|
12115 | 77 |
|
29376 | 78 |
use_thy "SVC_Oracle"; |
12115 | 79 |
|
28263 | 80 |
fun svc_enabled () = getenv "SVC_HOME" <> ""; |
81 |
fun if_svc_enabled f x = if svc_enabled () then f x else (); |
|
82 |
||
29377 | 83 |
if_svc_enabled use_thy "svc_test"; |
14459 | 84 |
|
29376 | 85 |
|
23191 | 86 |
(* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *) |
87 |
(* installed: *) |
|
29376 | 88 |
try use_thy "SAT_Examples"; |
17618
1330157e156a
new sat tactic imports resolution proofs from zChaff
webertj
parents:
17505
diff
changeset
|
89 |
|
23191 | 90 |
(* requires zChaff (or some other reasonably fast SAT solver) to be *) |
91 |
(* installed: *) |
|
18408 | 92 |
if getenv "ZCHAFF_HOME" <> "" then |
29376 | 93 |
use_thy "Sudoku" |
23191 | 94 |
else (); |
18408 | 95 |
|
25975
bcb1e9b7644b
Codegenerator vs. Codegenerator_Pretty: loaded sequentially, due to hazardous ML sections;
wenzelm
parents:
25963
diff
changeset
|
96 |
HTML.with_charset "utf-8" (no_document use_thys) ["Hebrew", "Chinese"]; |