author  wenzelm 
Tue, 06 Jan 2009 22:08:42 +0100  
changeset 29377  e6439dbfeee1 
parent 29376  2071939cf0fc 
child 29650  cc3958d31b1d 
permissions  rwrr 
12115  1 
(* Title: HOL/ex/ROOT.ML 
11586  2 

12115  3 
Miscellaneous examples for HigherOrder Logic. 
4 
*) 

5 

24528  6 
no_document use_thys [ 
24740  7 
"State_Monad", 
25963  8 
"Efficient_Nat_examples", 
9 
"ExecutableContent", 

10 
"FuncSet", 

11 
"Word", 

12 
"Eval_Examples", 

28243  13 
"Quickcheck", 
29376  14 
"Term_Of_Syntax", 
15 
"Codegenerator", 

16 
"Codegenerator_Pretty", 

29377  17 
"NormalForm", 
18 
"../NumberTheory/Factorization", 

19 
"../Library/BigO" 

25963  20 
]; 
21 

24478  22 
use_thys [ 
28021  23 
"Numeral", 
27679  24 
"ImperativeQuicksort", 
24478  25 
"Higher_Order_Logic", 
26 
"Abstract_NAT", 

27 
"Guess", 

28 
"Binary", 

29 
"Recdefs", 

30 
"Fundefs", 

25568  31 
"Induction_Scheme", 
24478  32 
"InductiveInvariant_examples", 
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 
"Lagrange", 

49 
"Groebner_Examples", 

50 
"MT", 

51 
"Unification", 

52 
"Commutative_RingEx", 

24740  53 
"Commutative_Ring_Complete", 
54 
"Primrec", 

55 
"Tarski", 

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

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

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

58 
"set", 
27436  59 
"Meson_Test", 
27742  60 
"Code_Antiq", 
29181
cc177742e607
renamed LexOrds.thy to Termination.thy; examples for sizechange method
krauss
parents:
28952
diff
changeset

61 
"Termination", 
29376  62 
"Coherent", 
63 
"Dense_Linear_Order_Ex", 

64 
"PresburgerEx", 

65 
"Reflected_Presburger", 

66 
"Reflection", 

29377  67 
"ReflectionEx", 
68 
"BinEx", 

69 
"Sqrt", 

70 
"Sqrt_Script", 

71 
"BigO_Complex", 

72 
"Arithmetic_Series_Complex", 

73 
"HarmonicSeries", 

74 
"MIR", 

75 
"ReflectedFerrack", 

76 
"Refute_Examples", 

77 
"Quickcheck_Examples" 

24478  78 
]; 
21256  79 

29376  80 
setmp Proofterm.proofs 2 use_thy "Hilbert_Classical"; 
24478  81 

12115  82 

29376  83 
use_thy "SVC_Oracle"; 
12115  84 

28263  85 
fun svc_enabled () = getenv "SVC_HOME" <> ""; 
86 
fun if_svc_enabled f x = if svc_enabled () then f x else (); 

87 

29377  88 
if_svc_enabled use_thy "svc_test"; 
14459  89 

29376  90 

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

29376  93 
try use_thy "SAT_Examples"; 
17618
1330157e156a
new sat tactic imports resolution proofs from zChaff
webertj
parents:
17505
diff
changeset

94 

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

18408  97 
if getenv "ZCHAFF_HOME" <> "" then 
29376  98 
use_thy "Sudoku" 
23191  99 
else (); 
18408  100 

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

101 
HTML.with_charset "utf8" (no_document use_thys) ["Hebrew", "Chinese"]; 