author  haftmann 
Fri, 25 Jan 2008 14:53:56 +0100  
changeset 25963  07e08dad8a77 
parent 25738  b091cbae3e2a 
child 25975  bcb1e9b7644b 
permissions  rwrr 
12115  1 
(* Title: HOL/ex/ROOT.ML 
2 
ID: $Id$ 

11586  3 

12115  4 
Miscellaneous examples for HigherOrder Logic. 
5 
*) 

6 

24528  7 
no_document use_thys [ 
24478  8 
"Parity", 
24740  9 
"GCD", 
10 
"Eval", 

11 
"State_Monad", 

25963  12 
"Efficient_Nat_examples", 
13 
"ExecutableContent", 

14 
"FuncSet", 

15 
"Word", 

16 
"Eval_Examples", 

17 
"Random" 

18 
]; 

19 

20 
no_document use_thys [ 

24740  21 
"Codegenerator", 
25963  22 
"Codegenerator_Pretty" 
24478  23 
]; 
24 

25 
use_thys [ 

26 
"Higher_Order_Logic", 

27 
"Abstract_NAT", 

28 
"Guess", 

29 
"Binary", 

30 
"Recdefs", 

31 
"Fundefs", 

25568  32 
"Induction_Scheme", 
24478  33 
"InductiveInvariant_examples", 
34 
"Locales", 

35 
"LocaleTest2", 

36 
"Records", 

37 
"MonoidGroup", 

38 
"BinEx", 

39 
"Hex_Bin_Examples", 

40 
"Antiquote", 

41 
"Multiquote", 

42 
"PER", 

43 
"NatSum", 

44 
"ThreeDivides", 

45 
"Intuitionistic", 

46 
"CTL", 

47 
"Arith_Examples", 

48 
"BT", 

49 
"MergeSort", 

50 
"Puzzle", 

51 
"Lagrange", 

52 
"Groebner_Examples", 

53 
"MT", 

54 
"Unification", 

55 
"Commutative_RingEx", 

24740  56 
"Commutative_Ring_Complete", 
57 
"Primrec", 

58 
"Tarski", 

25738
b091cbae3e2a
included meson/metis tests in simultaneous use_thys;
wenzelm
parents:
25568
diff
changeset

59 
"Adder", 
b091cbae3e2a
included meson/metis tests in simultaneous use_thys;
wenzelm
parents:
25568
diff
changeset

60 
"Classical", 
b091cbae3e2a
included meson/metis tests in simultaneous use_thys;
wenzelm
parents:
25568
diff
changeset

61 
"set", 
b091cbae3e2a
included meson/metis tests in simultaneous use_thys;
wenzelm
parents:
25568
diff
changeset

62 
"Meson_Test" 
24478  63 
]; 
21256  64 

25374  65 
setmp Proofterm.proofs 2 time_use_thy "Hilbert_Classical"; 
24478  66 

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

67 
time_use_thy "Dense_Linear_Order_Ex"; 
13880  68 
time_use_thy "PresburgerEx"; 
23808  69 
time_use_thy "Reflected_Presburger"; 
12115  70 

20325  71 
time_use_thy "Reflection"; 
12115  72 

23502  73 
time_use_thy "NBE"; 
74 

12869  75 
time_use_thy "SVC_Oracle"; 
12115  76 
if_svc_enabled time_use_thy "svc_test"; 
14459  77 

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

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

81 

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

18408  84 
if getenv "ZCHAFF_HOME" <> "" then 
85 
time_use_thy "Sudoku" 

23191  86 
else (); 
18408  87 

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

89 
time_use_thy "Quickcheck_Examples"; 
19832  90 
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

91 

17466  92 
HTML.with_charset "utf8" (no_document time_use_thy) "Hebrew"; 
17505  93 
HTML.with_charset "utf8" (no_document time_use_thy) "Chinese"; 