author  wenzelm 
Thu, 11 Jun 2009 12:50:20 +0200  
changeset 31555  318081898306 
parent 31381  b3a785a69538 
child 31556  ac0badf13d93 
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 
"FuncSet", 

10 
"Word", 

11 
"Eval_Examples", 

29808
b8b9d529663b
split of already properly working part of Quickcheck infrastructure
haftmann
parents:
29788
diff
changeset

12 
"Quickcheck_Generators", 
31378  13 
"Codegenerator_Test", 
14 
"Codegenerator_Pretty_Test", 

29377  15 
"NormalForm", 
30374
7311a1546d85
added predicate compiler, as formally checked prototype, not as user package
haftmann
parents:
30179
diff
changeset

16 
"../NumberTheory/Factorization", 
31555
318081898306
theory Predicate_Compile_ex: enable quick_and_dirty for now, to make it work with internal cheat_tac invocations;
wenzelm
parents:
31381
diff
changeset

17 
"Predicate_Compile" 
25963  18 
]; 
19 

31555
318081898306
theory Predicate_Compile_ex: enable quick_and_dirty for now, to make it work with internal cheat_tac invocations;
wenzelm
parents:
31381
diff
changeset

20 
setmp quick_and_dirty true use_thy "Predicate_Compile_ex"; 
318081898306
theory Predicate_Compile_ex: enable quick_and_dirty for now, to make it work with internal cheat_tac invocations;
wenzelm
parents:
31381
diff
changeset

21 

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

26 
"Guess", 

27 
"Binary", 

28 
"Recdefs", 

29 
"Fundefs", 

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

33 
"Records", 

34 
"MonoidGroup", 

35 
"BinEx", 

36 
"Hex_Bin_Examples", 

37 
"Antiquote", 

38 
"Multiquote", 

39 
"PER", 

40 
"NatSum", 

41 
"ThreeDivides", 

42 
"Intuitionistic", 

43 
"CTL", 

44 
"Arith_Examples", 

45 
"BT", 

46 
"MergeSort", 

47 
"Lagrange", 

48 
"Groebner_Examples", 

49 
"MT", 

50 
"Unification", 

51 
"Commutative_RingEx", 

24740  52 
"Commutative_Ring_Complete", 
53 
"Primrec", 

54 
"Tarski", 

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

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

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

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

59 
"Termination", 
29376  60 
"Coherent", 
61 
"PresburgerEx", 

29377  62 
"ReflectionEx", 
63 
"BinEx", 

64 
"Sqrt", 

65 
"Sqrt_Script", 

66 
"Arithmetic_Series_Complex", 

67 
"HarmonicSeries", 

68 
"Refute_Examples", 

29697
e8785144719d
Added Formal_Power_Series_Examples to HOLex image
chaieb
parents:
29650
diff
changeset

69 
"Quickcheck_Examples", 
31381  70 
"Formal_Power_Series_Examples", 
71 
"Landau" 

24478  72 
]; 
21256  73 

29376  74 
setmp Proofterm.proofs 2 use_thy "Hilbert_Classical"; 
24478  75 

12115  76 

29376  77 
use_thy "SVC_Oracle"; 
12115  78 

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

81 

29377  82 
if_svc_enabled use_thy "svc_test"; 
14459  83 

29376  84 

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

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

88 

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

18408  91 
if getenv "ZCHAFF_HOME" <> "" then 
29376  92 
use_thy "Sudoku" 
23191  93 
else (); 
18408  94 

30179  95 
HTML.with_charset "utf8" (no_document use_thys) 
96 
["Hebrew", "Chinese", "Serbian"]; 