author  wenzelm 
Sun, 10 Jun 2007 23:48:27 +0200  
changeset 23302  919d5c1fe509 
parent 23271  3f9ef4bf3f31 
child 23454  c54975167be9 
permissions  rwrr 
12115  1 
(* Title: HOL/ex/ROOT.ML 
2 
ID: $Id$ 

11586  3 

12115  4 
Miscellaneous examples for HigherOrder 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 proofgenerating 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 "utf8" (no_document time_use_thy) "Hebrew"; 
17505  94 
HTML.with_charset "utf8" (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"; 