author | Andreas Lochbihler |
Tue, 29 May 2012 15:31:58 +0200 | |
changeset 48028 | a5377f6d9f14 |
parent 47654 | f7df7104d13e |
child 48041 | d60f6b41bf2d |
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 [ |
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
40946
diff
changeset
|
7 |
"~~/src/HOL/Library/State_Monad", |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46585
diff
changeset
|
8 |
"Code_Nat_examples", |
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
40946
diff
changeset
|
9 |
"~~/src/HOL/Library/FuncSet", |
25963 | 10 |
"Eval_Examples", |
40946
3f697c636fa1
eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents:
40632
diff
changeset
|
11 |
"Normalization_by_Evaluation", |
3f697c636fa1
eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents:
40632
diff
changeset
|
12 |
"Hebrew", |
3f697c636fa1
eliminated fragile HTML.with_charset -- always use utf-8;
wenzelm
parents:
40632
diff
changeset
|
13 |
"Chinese", |
48028 | 14 |
"Serbian", |
15 |
"~~/src/HOL/Library/FinFun" |
|
25963 | 16 |
]; |
17 |
||
24478 | 18 |
use_thys [ |
40239
c4336e45f199
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
wenzelm
parents:
39395
diff
changeset
|
19 |
"Iff_Oracle", |
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
40239
diff
changeset
|
20 |
"Coercion_Examples", |
46558
fdb84c40e074
renamed ex/Numeral.thy to ex/Numeral_Representation.thy
huffman
parents:
46395
diff
changeset
|
21 |
"Numeral_Representation", |
24478 | 22 |
"Higher_Order_Logic", |
23 |
"Abstract_NAT", |
|
24 |
"Guess", |
|
25 |
"Binary", |
|
26 |
"Fundefs", |
|
33471 | 27 |
"Induction_Schema", |
24478 | 28 |
"LocaleTest2", |
29 |
"Records", |
|
37760 | 30 |
"While_Combinator_Example", |
24478 | 31 |
"MonoidGroup", |
32 |
"BinEx", |
|
33 |
"Hex_Bin_Examples", |
|
34 |
"Antiquote", |
|
35 |
"Multiquote", |
|
36 |
"PER", |
|
37 |
"NatSum", |
|
38 |
"ThreeDivides", |
|
39 |
"Intuitionistic", |
|
40 |
"CTL", |
|
41 |
"Arith_Examples", |
|
42 |
"BT", |
|
33436 | 43 |
"Tree23", |
24478 | 44 |
"MergeSort", |
45 |
"Lagrange", |
|
46 |
"Groebner_Examples", |
|
47 |
"MT", |
|
48 |
"Unification", |
|
24740 | 49 |
"Primrec", |
50 |
"Tarski", |
|
25738
b091cbae3e2a
included meson/metis tests in simultaneous use_thys;
wenzelm
parents:
25568
diff
changeset
|
51 |
"Classical", |
44276 | 52 |
"Set_Theory", |
27436 | 53 |
"Meson_Test", |
29181
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
28952
diff
changeset
|
54 |
"Termination", |
29376 | 55 |
"Coherent", |
56 |
"PresburgerEx", |
|
29377 | 57 |
"ReflectionEx", |
58 |
"Sqrt", |
|
59 |
"Sqrt_Script", |
|
32560 | 60 |
"Transfer_Ex", |
47654 | 61 |
"Transfer_Int_Nat", |
29377 | 62 |
"HarmonicSeries", |
63 |
"Refute_Examples", |
|
35160
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
33651
diff
changeset
|
64 |
"Landau", |
35163 | 65 |
"Execute_Choice", |
35328 | 66 |
"Summation", |
36793
27da0a27b76f
put construction of reals using Dedekind cuts in HOL/ex
huffman
parents:
35953
diff
changeset
|
67 |
"Gauge_Integration", |
40349 | 68 |
"Dedekind_Real", |
40632
dc55e6752046
adding birthday paradoxon from some abandoned drawer
bulwahn
parents:
40349
diff
changeset
|
69 |
"Quicksort", |
43238
04c886a1d1a5
renaming the formalisation of the birthday problem to a proper English name
bulwahn
parents:
42607
diff
changeset
|
70 |
"Birthday_Paradox", |
41582
c34415351b6d
experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
41465
diff
changeset
|
71 |
"List_to_Set_Comprehension_Examples", |
45224
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
45038
diff
changeset
|
72 |
"Seq", |
46395
f56be74d7f51
adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents:
45224
diff
changeset
|
73 |
"Simproc_Tests", |
48028 | 74 |
"Executable_Relation", |
75 |
"FinFunPred" |
|
24478 | 76 |
]; |
21256 | 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) *) |