author  haftmann 
Tue, 01 Jul 2008 07:58:17 +0200  
changeset 27421  7e458bd56860 
parent 26265  4b63b9e9b10d 
child 27436  9581777503e9 
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", 

26265  17 
"Quickcheck" 
25963  18 
]; 
19 

25975
bcb1e9b7644b
Codegenerator vs. Codegenerator_Pretty: loaded sequentially, due to hazardous ML sections;
wenzelm
parents:
25963
diff
changeset

20 
no_document use_thy "Codegenerator"; 
bcb1e9b7644b
Codegenerator vs. Codegenerator_Pretty: loaded sequentially, due to hazardous ML sections;
wenzelm
parents:
25963
diff
changeset

21 
no_document use_thy "Codegenerator_Pretty"; 
24478  22 

23 
use_thys [ 

24 
"Higher_Order_Logic", 

25 
"Abstract_NAT", 

26 
"Guess", 

27 
"Binary", 

28 
"Recdefs", 

29 
"Fundefs", 

25568  30 
"Induction_Scheme", 
24478  31 
"InductiveInvariant_examples", 
32 
"Locales", 

33 
"LocaleTest2", 

34 
"Records", 

35 
"MonoidGroup", 

36 
"BinEx", 

37 
"Hex_Bin_Examples", 

38 
"Antiquote", 

39 
"Multiquote", 

40 
"PER", 

41 
"NatSum", 

42 
"ThreeDivides", 

43 
"Intuitionistic", 

44 
"CTL", 

45 
"Arith_Examples", 

46 
"BT", 

47 
"MergeSort", 

48 
"Puzzle", 

49 
"Lagrange", 

50 
"Groebner_Examples", 

51 
"MT", 

52 
"Unification", 

53 
"Commutative_RingEx", 

24740  54 
"Commutative_Ring_Complete", 
55 
"Primrec", 

56 
"Tarski", 

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

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

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

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

60 
"Meson_Test" 
24478  61 
]; 
21256  62 

25374  63 
setmp Proofterm.proofs 2 time_use_thy "Hilbert_Classical"; 
24478  64 

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

65 
time_use_thy "Dense_Linear_Order_Ex"; 
13880  66 
time_use_thy "PresburgerEx"; 
23808  67 
time_use_thy "Reflected_Presburger"; 
12115  68 

20325  69 
time_use_thy "Reflection"; 
12115  70 

12869  71 
time_use_thy "SVC_Oracle"; 
12115  72 
if_svc_enabled time_use_thy "svc_test"; 
14459  73 

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

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

77 

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

18408  80 
if getenv "ZCHAFF_HOME" <> "" then 
81 
time_use_thy "Sudoku" 

23191  82 
else (); 
18408  83 

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

85 
time_use_thy "Quickcheck_Examples"; 
19832  86 
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

87 

25975
bcb1e9b7644b
Codegenerator vs. Codegenerator_Pretty: loaded sequentially, due to hazardous ML sections;
wenzelm
parents:
25963
diff
changeset

88 
HTML.with_charset "utf8" (no_document use_thys) ["Hebrew", "Chinese"]; 
bcb1e9b7644b
Codegenerator vs. Codegenerator_Pretty: loaded sequentially, due to hazardous ML sections;
wenzelm
parents:
25963
diff
changeset

89 

27421  90 
no_document use_thys [ 
91 
"../NumberTheory/Factorization", 

92 
"../Library/BigO", 

93 
"../Library/NatPair" 

94 
]; 

95 

96 
use_thys [ 

97 
"../Complex/ex/BinEx", 

98 
"../Complex/ex/Sqrt", 

99 
"../Complex/ex/Sqrt_Script", 

100 
"../Complex/ex/NSPrimes", 

101 
"../Complex/ex/BigO_Complex", 

102 

103 
"../Complex/ex/Arithmetic_Series_Complex", 

104 
"../Complex/ex/HarmonicSeries", 

105 

106 
"../Complex/ex/DenumRat", 

107 

108 
"../Complex/ex/MIR", 

109 
"../Complex/ex/ReflectedFerrack" 

110 
]; 

111 