author  wenzelm 
Wed, 02 Jun 2010 13:18:21 +0200  
changeset 37280  0fb011773adc 
parent 36962  5fb251d1c32f 
child 37695  71e84a203c19 
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 
"Eval_Examples", 

31378  11 
"Codegenerator_Test", 
12 
"Codegenerator_Pretty_Test", 

35953
0460ff79bb52
moved further predicate compile files to HOLLibrary
bulwahn
parents:
35950
diff
changeset

13 
"NormalForm" 
25963  14 
]; 
15 

24478  16 
use_thys [ 
28021  17 
"Numeral", 
24478  18 
"Higher_Order_Logic", 
19 
"Abstract_NAT", 

20 
"Guess", 

21 
"Binary", 

22 
"Recdefs", 

23 
"Fundefs", 

33471  24 
"Induction_Schema", 
24478  25 
"InductiveInvariant_examples", 
26 
"LocaleTest2", 

27 
"Records", 

28 
"MonoidGroup", 

29 
"BinEx", 

30 
"Hex_Bin_Examples", 

31 
"Antiquote", 

32 
"Multiquote", 

33 
"PER", 

34 
"NatSum", 

35 
"ThreeDivides", 

36 
"Intuitionistic", 

37 
"CTL", 

38 
"Arith_Examples", 

39 
"BT", 

33436  40 
"Tree23", 
24478  41 
"MergeSort", 
42 
"Lagrange", 

43 
"Groebner_Examples", 

44 
"MT", 

45 
"Unification", 

24740  46 
"Primrec", 
47 
"Tarski", 

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

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

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

51 
"Termination", 
29376  52 
"Coherent", 
53 
"PresburgerEx", 

29377  54 
"ReflectionEx", 
55 
"BinEx", 

56 
"Sqrt", 

57 
"Sqrt_Script", 

32560  58 
"Transfer_Ex", 
29377  59 
"Arithmetic_Series_Complex", 
60 
"HarmonicSeries", 

61 
"Refute_Examples", 

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

62 
"Quickcheck_Examples", 
35160
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
33651
diff
changeset

63 
"Landau", 
35163  64 
"Execute_Choice", 
35328  65 
"Summation", 
36793
27da0a27b76f
put construction of reals using Dedekind cuts in HOL/ex
huffman
parents:
35953
diff
changeset

66 
"Gauge_Integration", 
27da0a27b76f
put construction of reals using Dedekind cuts in HOL/ex
huffman
parents:
35953
diff
changeset

67 
"Dedekind_Real" 
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 

37280
0fb011773adc
Hilbert_Classical: disable multithreading altogether, otherwise proof normalization will fork futures independently of Goal.parallel_proofs;
wenzelm
parents:
36962
diff
changeset

73 
(setmp_noncritical proofs 2 (setmp_noncritical Multithreading.max_threads 1 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) *) 