|
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@41661
|
7 |
"~~/src/HOL/Library/State_Monad",
|
|
haftmann@25963
|
8 |
"Efficient_Nat_examples",
|
|
wenzelm@41661
|
9 |
"~~/src/HOL/Library/FuncSet",
|
|
haftmann@25963
|
10 |
"Eval_Examples",
|
|
wenzelm@41194
|
11 |
"Normalization_by_Evaluation",
|
|
wenzelm@41194
|
12 |
"Hebrew",
|
|
wenzelm@41194
|
13 |
"Chinese",
|
|
wenzelm@41194
|
14 |
"Serbian"
|
|
haftmann@25963
|
15 |
];
|
|
haftmann@25963
|
16 |
|
|
wenzelm@24478
|
17 |
use_thys [
|
|
wenzelm@40495
|
18 |
"Iff_Oracle",
|
|
wenzelm@40528
|
19 |
"Coercion_Examples",
|
|
haftmann@28021
|
20 |
"Numeral",
|
|
wenzelm@24478
|
21 |
"Higher_Order_Logic",
|
|
wenzelm@24478
|
22 |
"Abstract_NAT",
|
|
wenzelm@24478
|
23 |
"Guess",
|
|
wenzelm@24478
|
24 |
"Binary",
|
|
wenzelm@24478
|
25 |
"Recdefs",
|
|
wenzelm@24478
|
26 |
"Fundefs",
|
|
krauss@33471
|
27 |
"Induction_Schema",
|
|
wenzelm@24478
|
28 |
"InductiveInvariant_examples",
|
|
wenzelm@24478
|
29 |
"LocaleTest2",
|
|
wenzelm@24478
|
30 |
"Records",
|
|
krauss@37759
|
31 |
"While_Combinator_Example",
|
|
wenzelm@24478
|
32 |
"MonoidGroup",
|
|
wenzelm@24478
|
33 |
"BinEx",
|
|
wenzelm@24478
|
34 |
"Hex_Bin_Examples",
|
|
wenzelm@24478
|
35 |
"Antiquote",
|
|
wenzelm@24478
|
36 |
"Multiquote",
|
|
wenzelm@24478
|
37 |
"PER",
|
|
wenzelm@24478
|
38 |
"NatSum",
|
|
wenzelm@24478
|
39 |
"ThreeDivides",
|
|
wenzelm@24478
|
40 |
"Intuitionistic",
|
|
wenzelm@24478
|
41 |
"CTL",
|
|
wenzelm@24478
|
42 |
"Arith_Examples",
|
|
wenzelm@24478
|
43 |
"BT",
|
|
nipkow@33425
|
44 |
"Tree23",
|
|
wenzelm@24478
|
45 |
"MergeSort",
|
|
wenzelm@24478
|
46 |
"Lagrange",
|
|
wenzelm@24478
|
47 |
"Groebner_Examples",
|
|
wenzelm@24478
|
48 |
"MT",
|
|
wenzelm@24478
|
49 |
"Unification",
|
|
wenzelm@24740
|
50 |
"Primrec",
|
|
wenzelm@24740
|
51 |
"Tarski",
|
|
wenzelm@25738
|
52 |
"Classical",
|
|
wenzelm@25738
|
53 |
"set",
|
|
haftmann@27436
|
54 |
"Meson_Test",
|
|
krauss@29181
|
55 |
"Termination",
|
|
wenzelm@29376
|
56 |
"Coherent",
|
|
wenzelm@29376
|
57 |
"PresburgerEx",
|
|
wenzelm@29377
|
58 |
"ReflectionEx",
|
|
wenzelm@29377
|
59 |
"BinEx",
|
|
wenzelm@29377
|
60 |
"Sqrt",
|
|
wenzelm@29377
|
61 |
"Sqrt_Script",
|
|
haftmann@32560
|
62 |
"Transfer_Ex",
|
|
wenzelm@29377
|
63 |
"Arithmetic_Series_Complex",
|
|
wenzelm@29377
|
64 |
"HarmonicSeries",
|
|
wenzelm@29377
|
65 |
"Refute_Examples",
|
|
chaieb@29697
|
66 |
"Quickcheck_Examples",
|
|
bulwahn@38157
|
67 |
"Quickcheck_Lattice_Examples",
|
|
haftmann@35160
|
68 |
"Landau",
|
|
haftmann@35163
|
69 |
"Execute_Choice",
|
|
hoelzl@35328
|
70 |
"Summation",
|
|
huffman@36787
|
71 |
"Gauge_Integration",
|
|
haftmann@40590
|
72 |
"Dedekind_Real",
|
|
bulwahn@40880
|
73 |
"Quicksort",
|
|
bulwahn@41697
|
74 |
"Birthday_Paradoxon",
|
|
haftmann@41829
|
75 |
"List_to_Set_Comprehension_Examples",
|
|
wenzelm@42949
|
76 |
"Set_Algebras"
|
|
wenzelm@24478
|
77 |
];
|
|
wenzelm@21256
|
78 |
|
|
wenzelm@42949
|
79 |
Unsynchronized.setmp Proofterm.proofs (! Proofterm.proofs)
|
|
wenzelm@42949
|
80 |
use_thy "TPTP";
|
|
wenzelm@42949
|
81 |
|
|
wenzelm@42823
|
82 |
if getenv "ISABELLE_GHC" = "" then ()
|
|
bulwahn@42803
|
83 |
else use_thy "Quickcheck_Narrowing_Examples";
|
|
bulwahn@42785
|
84 |
|
|
wenzelm@32428
|
85 |
use_thy "SVC_Oracle";
|
|
wenzelm@32428
|
86 |
if getenv "SVC_HOME" = "" then ()
|
|
wenzelm@32428
|
87 |
else use_thy "svc_test";
|
|
wenzelm@12115
|
88 |
|
|
wenzelm@32428
|
89 |
(*requires zChaff (or some other reasonably fast SAT solver)*)
|
|
wenzelm@32428
|
90 |
if getenv "ZCHAFF_HOME" = "" then ()
|
|
wenzelm@32428
|
91 |
else use_thy "Sudoku";
|
|
webertj@18408
|
92 |
|
|
wenzelm@33546
|
93 |
(*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
|
|
wenzelm@33546
|
94 |
(*global side-effects ahead!*)
|
|
wenzelm@33546
|
95 |
try use_thy "SAT_Examples"; (* FIXME try!? (not really a proper test) *)
|