author  wenzelm 
Tue, 10 Nov 2009 13:17:50 +0100  
changeset 33546  5e2d381b0695 
parent 33471  5aef13872723 
child 33651  e4aad90618ad 
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", 

31378  12 
"Codegenerator_Test", 
13 
"Codegenerator_Pretty_Test", 

29377  14 
"NormalForm", 
31129
d2cead76fca2
split Predicate_Compile examples into separate theory
haftmann
parents:
30740
diff
changeset

15 
"Predicate_Compile", 
d2cead76fca2
split Predicate_Compile examples into separate theory
haftmann
parents:
30740
diff
changeset

16 
"Predicate_Compile_ex" 
25963  17 
]; 
18 

24478  19 
use_thys [ 
28021  20 
"Numeral", 
24478  21 
"Higher_Order_Logic", 
22 
"Abstract_NAT", 

23 
"Guess", 

24 
"Binary", 

25 
"Recdefs", 

26 
"Fundefs", 

33471  27 
"Induction_Schema", 
24478  28 
"InductiveInvariant_examples", 
29 
"LocaleTest2", 

30 
"Records", 

31 
"MonoidGroup", 

32 
"BinEx", 

33 
"Hex_Bin_Examples", 

34 
"Antiquote", 

35 
"Multiquote", 

36 
"PER", 

37 
"NatSum", 

38 
"ThreeDivides", 

39 
"Intuitionistic", 

40 
"CTL", 

41 
"Arith_Examples", 

42 
"BT", 

33436  43 
"Tree23", 
24478  44 
"MergeSort", 
45 
"Lagrange", 

46 
"Groebner_Examples", 

47 
"MT", 

48 
"Unification", 

24740  49 
"Primrec", 
50 
"Tarski", 

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

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

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

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

55 
"Termination", 
29376  56 
"Coherent", 
57 
"PresburgerEx", 

29377  58 
"ReflectionEx", 
59 
"BinEx", 

60 
"Sqrt", 

61 
"Sqrt_Script", 

32560  62 
"Transfer_Ex", 
29377  63 
"Arithmetic_Series_Complex", 
64 
"HarmonicSeries", 

65 
"Refute_Examples", 

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

66 
"Quickcheck_Examples", 
31381  67 
"Landau" 
24478  68 
]; 
21256  69 

33546
5e2d381b0695
try SAT_Examples last, to minimize impact of global sideeffects;
wenzelm
parents:
33471
diff
changeset

70 
HTML.with_charset "utf8" (no_document use_thys) 
5e2d381b0695
try SAT_Examples last, to minimize impact of global sideeffects;
wenzelm
parents:
33471
diff
changeset

71 
["Hebrew", "Chinese", "Serbian"]; 
5e2d381b0695
try SAT_Examples last, to minimize impact of global sideeffects;
wenzelm
parents:
33471
diff
changeset

72 

32615
20f1edc87b7d
Hilbert_Classical: more precise control of parallel_proofs;
wenzelm
parents:
32560
diff
changeset

73 
(setmp_noncritical proofs 2 (setmp_noncritical Goal.parallel_proofs 0 use_thy)) 
32256
8721c74c5382
Hilbert_Classical: sequential loading due to @{prf}, which joins within a critical section (via options);
wenzelm
parents:
32254
diff
changeset

74 
"Hilbert_Classical"; 
24478  75 

29376  76 
use_thy "SVC_Oracle"; 
32428
700ed1f4c576
SAT_Examples: removed obsolete Future.shutdown() workaround  internal exception propagation should now work reliably;
wenzelm
parents:
32259
diff
changeset

77 
if getenv "SVC_HOME" = "" then () 
700ed1f4c576
SAT_Examples: removed obsolete Future.shutdown() workaround  internal exception propagation should now work reliably;
wenzelm
parents:
32259
diff
changeset

78 
else use_thy "svc_test"; 
29376  79 

32428
700ed1f4c576
SAT_Examples: removed obsolete Future.shutdown() workaround  internal exception propagation should now work reliably;
wenzelm
parents:
32259
diff
changeset

80 
(*requires zChaff (or some other reasonably fast SAT solver)*) 
700ed1f4c576
SAT_Examples: removed obsolete Future.shutdown() workaround  internal exception propagation should now work reliably;
wenzelm
parents:
32259
diff
changeset

81 
if getenv "ZCHAFF_HOME" = "" then () 
700ed1f4c576
SAT_Examples: removed obsolete Future.shutdown() workaround  internal exception propagation should now work reliably;
wenzelm
parents:
32259
diff
changeset

82 
else use_thy "Sudoku"; 
18408  83 

33546
5e2d381b0695
try SAT_Examples last, to minimize impact of global sideeffects;
wenzelm
parents:
33471
diff
changeset

84 
(*requires a proofgenerating SAT solver (zChaff or MiniSAT)*) 
5e2d381b0695
try SAT_Examples last, to minimize impact of global sideeffects;
wenzelm
parents:
33471
diff
changeset

85 
(*global sideeffects ahead!*) 
5e2d381b0695
try SAT_Examples last, to minimize impact of global sideeffects;
wenzelm
parents:
33471
diff
changeset

86 
try use_thy "SAT_Examples"; (* FIXME try!? (not really a proper test) *) 