author | chaieb |
Mon, 11 Jun 2007 11:06:00 +0200 | |
changeset 23314 | 6894137e854a |
parent 23302 | 919d5c1fe509 |
child 23454 | c54975167be9 |
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 |
||
21256 | 7 |
no_document use_thy "Parity"; |
8 |
no_document use_thy "GCD"; |
|
9 |
||
19438 | 10 |
no_document time_use_thy "Classpackage"; |
23271 | 11 |
|
12 |
no_document time_use_thy "Eval"; |
|
13 |
time_use_thy "Eval_Examples"; |
|
14 |
||
15 |
no_document time_use_thy "State_Monad"; |
|
16 |
no_document time_use_thy "Pretty_Int"; |
|
17 |
time_use_thy "Random"; |
|
18 |
||
19 |
no_document time_use_thy "ExecutableRat"; |
|
20 |
no_document time_use_thy "EfficientNat"; |
|
21 |
time_use_thy "Codegenerator_Rat"; |
|
21911
e29bcab0c81c
added OCaml code generation (without dictionaries)
haftmann
parents:
21256
diff
changeset
|
22 |
no_document time_use_thy "Codegenerator"; |
19438 | 23 |
|
12360 | 24 |
time_use_thy "Higher_Order_Logic"; |
19085 | 25 |
time_use_thy "Abstract_NAT"; |
19997 | 26 |
time_use_thy "Guess"; |
22140 | 27 |
time_use_thy "Binary"; |
12360 | 28 |
|
12115 | 29 |
time_use_thy "Recdefs"; |
22167 | 30 |
time_use_thy "Fundefs"; |
14244
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
14220
diff
changeset
|
31 |
time_use_thy "InductiveInvariant_examples"; |
12115 | 32 |
time_use_thy "Primrec"; |
12276 | 33 |
time_use_thy "Locales"; |
22657 | 34 |
time_use_thy "LocaleTest2"; |
12115 | 35 |
time_use_thy "Records"; |
36 |
time_use_thy "MonoidGroup"; |
|
37 |
time_use_thy "BinEx"; |
|
20866 | 38 |
time_use_thy "Hex_Bin_Examples"; |
12115 | 39 |
setmp proofs 2 time_use_thy "Hilbert_Classical"; |
40 |
time_use_thy "Antiquote"; |
|
41 |
time_use_thy "Multiquote"; |
|
42 |
||
20812 | 43 |
time_use_thy "PER"; |
12115 | 44 |
time_use_thy "NatSum"; |
19022
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
18678
diff
changeset
|
45 |
time_use_thy "ThreeDivides"; |
12450
1162b280700a
Added example file for intuitionistic logic (taken from FOL).
berghofe
parents:
12360
diff
changeset
|
46 |
time_use_thy "Intuitionistic"; |
14220
4dc132902672
Merging of ex/cla.ML and ex/mesontest.ML to ex/Classical.thy
paulson
parents:
13880
diff
changeset
|
47 |
time_use_thy "Classical"; |
15871 | 48 |
time_use_thy "CTL"; |
12115 | 49 |
time_use_thy "mesontest2"; |
23193 | 50 |
time_use_thy "Arith_Examples"; |
13880 | 51 |
time_use_thy "PresburgerEx"; |
23302
919d5c1fe509
disabled theory "Reflected_Presburger" for smlnj (temporarily);
wenzelm
parents:
23271
diff
changeset
|
52 |
if String.isPrefix "smlnj" ml_system then () (* FIXME tmp *) |
919d5c1fe509
disabled theory "Reflected_Presburger" for smlnj (temporarily);
wenzelm
parents:
23271
diff
changeset
|
53 |
else time_use_thy "Reflected_Presburger"; |
12115 | 54 |
time_use_thy "BT"; |
55 |
time_use_thy "InSort"; |
|
56 |
time_use_thy "Qsort"; |
|
13200 | 57 |
time_use_thy "MergeSort"; |
12115 | 58 |
time_use_thy "Puzzle"; |
59 |
||
14603 | 60 |
time_use_thy "Lagrange"; |
23271 | 61 |
time_use_thy "Groebner_Examples"; |
62 |
||
17378
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
15871
diff
changeset
|
63 |
time_use_thy "Commutative_RingEx"; |
105519771c67
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
chaieb
parents:
15871
diff
changeset
|
64 |
time_use_thy "Commutative_Ring_Complete"; |
20325 | 65 |
time_use_thy "Reflection"; |
12115 | 66 |
|
67 |
time_use_thy "set"; |
|
68 |
time_use_thy "MT"; |
|
14569 | 69 |
|
70 |
no_document use_thy "FuncSet"; |
|
12115 | 71 |
time_use_thy "Tarski"; |
72 |
||
12869 | 73 |
time_use_thy "SVC_Oracle"; |
12115 | 74 |
if_svc_enabled time_use_thy "svc_test"; |
14459 | 75 |
|
23191 | 76 |
(* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *) |
77 |
(* installed: *) |
|
18678 | 78 |
try time_use_thy "SAT_Examples"; |
17618
1330157e156a
new sat tactic imports resolution proofs from zChaff
webertj
parents:
17505
diff
changeset
|
79 |
|
23191 | 80 |
(* requires zChaff (or some other reasonably fast SAT solver) to be *) |
81 |
(* installed: *) |
|
18408 | 82 |
if getenv "ZCHAFF_HOME" <> "" then |
83 |
time_use_thy "Sudoku" |
|
23191 | 84 |
else (); |
18408 | 85 |
|
14462 | 86 |
time_use_thy "Refute_Examples"; |
14592
dd1a2905ea73
Added theory with examples for quickcheck command.
berghofe
parents:
14569
diff
changeset
|
87 |
time_use_thy "Quickcheck_Examples"; |
19832 | 88 |
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
|
89 |
|
14569 | 90 |
no_document use_thy "Word"; |
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
14482
diff
changeset
|
91 |
time_use_thy "Adder"; |
14569 | 92 |
|
17466 | 93 |
HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew"; |
17505 | 94 |
HTML.with_charset "utf-8" (no_document time_use_thy) "Chinese"; |
22999
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
22657
diff
changeset
|
95 |
|
c1ce129e6f9c
Added unification case study (using new function package)
krauss
parents:
22657
diff
changeset
|
96 |
time_use_thy "Unification"; |