author  wenzelm 
Wed, 29 Aug 2007 20:18:23 +0200  
changeset 24478  fb5e3fcfc10c 
parent 24195  7d1a16c77f7c 
child 24528  e8197c9f1b5c 
permissions  rwrr 
12115  1 
(* Title: HOL/ex/ROOT.ML 
2 
ID: $Id$ 

11586  3 

12115  4 
Miscellaneous examples for HigherOrder Logic. 
5 
*) 

6 

24478  7 
no_document use_thys [ 
8 
"Parity", 

9 
"GCD" 

10 
]; 

11 

12 
use_thys [ 

13 
"Higher_Order_Logic", 

14 
"Abstract_NAT", 

15 
"Guess", 

16 
"Binary", 

17 
"Recdefs", 

18 
"Fundefs", 

19 
"InductiveInvariant_examples", 

20 
"Locales", 

21 
"LocaleTest2", 

22 
"Records", 

23 
"MonoidGroup", 

24 
"BinEx", 

25 
"Hex_Bin_Examples", 

26 
"Antiquote", 

27 
"Multiquote", 

28 
"PER", 

29 
"NatSum", 

30 
"ThreeDivides", 

31 
"Intuitionistic", 

32 
"CTL", 

33 
"Arith_Examples", 

34 
"BT", 

35 
"InSort", 

36 
"Qsort", 

37 
"MergeSort", 

38 
"Puzzle", 

39 
"Lagrange", 

40 
"Groebner_Examples", 

41 
"MT", 

42 
"Unification", 

43 
"Commutative_RingEx", 

44 
"Commutative_Ring_Complete" 

45 
]; 

21256  46 

19438  47 
no_document time_use_thy "Classpackage"; 
23271  48 

49 
no_document time_use_thy "Eval"; 

50 
time_use_thy "Eval_Examples"; 

51 

52 
no_document time_use_thy "State_Monad"; 

53 
no_document time_use_thy "Pretty_Int"; 

54 
time_use_thy "Random"; 

55 

23854  56 
no_document time_use_thy "Executable_Rat"; 
57 
no_document time_use_thy "Efficient_Nat"; 

21911
e29bcab0c81c
added OCaml code generation (without dictionaries)
haftmann
parents:
21256
diff
changeset

58 
no_document time_use_thy "Codegenerator"; 
24195  59 
no_document time_use_thy "Codegenerator_Pretty"; 
19438  60 

12360  61 

24478  62 
setmp proofs 2 time_use_thy "Hilbert_Classical"; 
63 

12115  64 
time_use_thy "Primrec"; 
24478  65 
time_use_thy "Classical"; 
66 
time_use_thy "set"; 

12115  67 

24127  68 
time_use_thy "Meson_Test"; 
23454
c54975167be9
replaced Real/FerranteRackoff tool by generic version in Main HOL;
wenzelm
parents:
23302
diff
changeset

69 
time_use_thy "Dense_Linear_Order_Ex"; 
13880  70 
time_use_thy "PresburgerEx"; 
23808  71 
time_use_thy "Reflected_Presburger"; 
12115  72 

20325  73 
time_use_thy "Reflection"; 
12115  74 

23502  75 
time_use_thy "NBE"; 
76 

14569  77 
no_document use_thy "FuncSet"; 
12115  78 
time_use_thy "Tarski"; 
79 

12869  80 
time_use_thy "SVC_Oracle"; 
12115  81 
if_svc_enabled time_use_thy "svc_test"; 
14459  82 

23191  83 
(* requires a proofgenerating SAT solver (zChaff or MiniSAT) to be *) 
84 
(* installed: *) 

18678  85 
try time_use_thy "SAT_Examples"; 
17618
1330157e156a
new sat tactic imports resolution proofs from zChaff
webertj
parents:
17505
diff
changeset

86 

23191  87 
(* requires zChaff (or some other reasonably fast SAT solver) to be *) 
88 
(* installed: *) 

18408  89 
if getenv "ZCHAFF_HOME" <> "" then 
90 
time_use_thy "Sudoku" 

23191  91 
else (); 
18408  92 

14462  93 
time_use_thy "Refute_Examples"; 
14592
dd1a2905ea73
Added theory with examples for quickcheck command.
berghofe
parents:
14569
diff
changeset

94 
time_use_thy "Quickcheck_Examples"; 
19832  95 
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

96 

14569  97 
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

98 
time_use_thy "Adder"; 
14569  99 

17466  100 
HTML.with_charset "utf8" (no_document time_use_thy) "Hebrew"; 
17505  101 
HTML.with_charset "utf8" (no_document time_use_thy) "Chinese"; 