|
wenzelm@12115
|
1 |
(* Title: HOL/ex/ROOT.ML
|
|
wenzelm@12115
|
2 |
ID: $Id$
|
|
wenzelm@11586
|
3 |
|
|
wenzelm@12115
|
4 |
Miscellaneous examples for Higher-Order Logic.
|
|
wenzelm@12115
|
5 |
*)
|
|
wenzelm@12115
|
6 |
|
|
wenzelm@24528
|
7 |
no_document use_thys [
|
|
wenzelm@24478
|
8 |
"Parity",
|
|
wenzelm@24740
|
9 |
"GCD",
|
|
wenzelm@24740
|
10 |
"Classpackage",
|
|
wenzelm@24740
|
11 |
"Eval",
|
|
wenzelm@24740
|
12 |
"State_Monad",
|
|
wenzelm@24740
|
13 |
"Pretty_Int",
|
|
wenzelm@24740
|
14 |
"Efficient_Nat",
|
|
wenzelm@24740
|
15 |
"Codegenerator",
|
|
wenzelm@24740
|
16 |
"Codegenerator_Pretty",
|
|
wenzelm@24740
|
17 |
"FuncSet",
|
|
wenzelm@24740
|
18 |
"Word"
|
|
wenzelm@24478
|
19 |
];
|
|
wenzelm@24478
|
20 |
|
|
wenzelm@24478
|
21 |
use_thys [
|
|
wenzelm@24478
|
22 |
"Higher_Order_Logic",
|
|
wenzelm@24478
|
23 |
"Abstract_NAT",
|
|
wenzelm@24478
|
24 |
"Guess",
|
|
wenzelm@24478
|
25 |
"Binary",
|
|
wenzelm@24478
|
26 |
"Recdefs",
|
|
wenzelm@24478
|
27 |
"Fundefs",
|
|
wenzelm@24478
|
28 |
"InductiveInvariant_examples",
|
|
wenzelm@24478
|
29 |
"Locales",
|
|
wenzelm@24478
|
30 |
"LocaleTest2",
|
|
wenzelm@24478
|
31 |
"Records",
|
|
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",
|
|
wenzelm@24478
|
44 |
"MergeSort",
|
|
wenzelm@24478
|
45 |
"Puzzle",
|
|
wenzelm@24478
|
46 |
"Lagrange",
|
|
wenzelm@24478
|
47 |
"Groebner_Examples",
|
|
wenzelm@24478
|
48 |
"MT",
|
|
wenzelm@24478
|
49 |
"Unification",
|
|
wenzelm@24478
|
50 |
"Commutative_RingEx",
|
|
wenzelm@24740
|
51 |
"Commutative_Ring_Complete",
|
|
wenzelm@24740
|
52 |
"Eval_Examples",
|
|
wenzelm@24740
|
53 |
"Random",
|
|
wenzelm@24740
|
54 |
"Primrec",
|
|
wenzelm@24740
|
55 |
"Tarski",
|
|
wenzelm@24740
|
56 |
"Adder"
|
|
wenzelm@24478
|
57 |
];
|
|
wenzelm@21256
|
58 |
|
|
wenzelm@24478
|
59 |
setmp proofs 2 time_use_thy "Hilbert_Classical";
|
|
wenzelm@24478
|
60 |
|
|
wenzelm@24478
|
61 |
time_use_thy "Classical";
|
|
wenzelm@24478
|
62 |
time_use_thy "set";
|
|
wenzelm@12115
|
63 |
|
|
wenzelm@24127
|
64 |
time_use_thy "Meson_Test";
|
|
wenzelm@23454
|
65 |
time_use_thy "Dense_Linear_Order_Ex";
|
|
berghofe@13880
|
66 |
time_use_thy "PresburgerEx";
|
|
haftmann@23808
|
67 |
time_use_thy "Reflected_Presburger";
|
|
wenzelm@12115
|
68 |
|
|
wenzelm@20325
|
69 |
time_use_thy "Reflection";
|
|
wenzelm@12115
|
70 |
|
|
nipkow@23502
|
71 |
time_use_thy "NBE";
|
|
nipkow@23502
|
72 |
|
|
wenzelm@12869
|
73 |
time_use_thy "SVC_Oracle";
|
|
wenzelm@12115
|
74 |
if_svc_enabled time_use_thy "svc_test";
|
|
webertj@14459
|
75 |
|
|
webertj@23191
|
76 |
(* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)
|
|
webertj@23191
|
77 |
(* installed: *)
|
|
wenzelm@18678
|
78 |
try time_use_thy "SAT_Examples";
|
|
webertj@17618
|
79 |
|
|
webertj@23191
|
80 |
(* requires zChaff (or some other reasonably fast SAT solver) to be *)
|
|
webertj@23191
|
81 |
(* installed: *)
|
|
webertj@18408
|
82 |
if getenv "ZCHAFF_HOME" <> "" then
|
|
webertj@18408
|
83 |
time_use_thy "Sudoku"
|
|
webertj@23191
|
84 |
else ();
|
|
webertj@18408
|
85 |
|
|
webertj@14462
|
86 |
time_use_thy "Refute_Examples";
|
|
berghofe@14592
|
87 |
time_use_thy "Quickcheck_Examples";
|
|
nipkow@19832
|
88 |
no_document time_use_thy "NormalForm";
|
|
skalberg@14494
|
89 |
|
|
wenzelm@17466
|
90 |
HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew";
|
|
wenzelm@17505
|
91 |
HTML.with_charset "utf-8" (no_document time_use_thy) "Chinese";
|