author  bulwahn 
Fri, 11 Mar 2011 10:37:45 +0100  
changeset 41914  4ef7e6e317fa 
parent 41911  c6e66b32ce16 
child 41932  e8f113ce8a94 
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 [ 
41413
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
40946
diff
changeset

7 
"~~/src/HOL/Library/State_Monad", 
25963  8 
"Efficient_Nat_examples", 
41413
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
40946
diff
changeset

9 
"~~/src/HOL/Library/FuncSet", 
25963  10 
"Eval_Examples", 
40946
3f697c636fa1
eliminated fragile HTML.with_charset  always use utf8;
wenzelm
parents:
40632
diff
changeset

11 
"Normalization_by_Evaluation", 
3f697c636fa1
eliminated fragile HTML.with_charset  always use utf8;
wenzelm
parents:
40632
diff
changeset

12 
"Hebrew", 
3f697c636fa1
eliminated fragile HTML.with_charset  always use utf8;
wenzelm
parents:
40632
diff
changeset

13 
"Chinese", 
3f697c636fa1
eliminated fragile HTML.with_charset  always use utf8;
wenzelm
parents:
40632
diff
changeset

14 
"Serbian" 
25963  15 
]; 
16 

24478  17 
use_thys [ 
40239
c4336e45f199
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isarref;
wenzelm
parents:
39395
diff
changeset

18 
"Iff_Oracle", 
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21Oct2010).
wenzelm
parents:
40239
diff
changeset

19 
"Coercion_Examples", 
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", 

37760  31 
"While_Combinator_Example", 
24478  32 
"MonoidGroup", 
33 
"BinEx", 

34 
"Hex_Bin_Examples", 

35 
"Antiquote", 

36 
"Multiquote", 

37 
"PER", 

38 
"NatSum", 

39 
"ThreeDivides", 

40 
"Intuitionistic", 

41 
"CTL", 

42 
"Arith_Examples", 

43 
"BT", 

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

47 
"Groebner_Examples", 

48 
"MT", 

49 
"Unification", 

24740  50 
"Primrec", 
51 
"Tarski", 

25738
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", 
37917  67 
"Quickcheck_Lattice_Examples", 
35160
6eb2b6c1d2d5
a draft for an example how to turn specifications involving choice executable
haftmann
parents:
33651
diff
changeset

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

71 
"Gauge_Integration", 
40349  72 
"Dedekind_Real", 
40632
dc55e6752046
adding birthday paradoxon from some abandoned drawer
bulwahn
parents:
40349
diff
changeset

73 
"Quicksort", 
41465
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
41413
diff
changeset

74 
"Birthday_Paradoxon", 
41582
c34415351b6d
experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
41465
diff
changeset

75 
"List_to_Set_Comprehension_Examples", 
41914
4ef7e6e317fa
only testing theory LSC_Examples when GHC is installed on the machine
bulwahn
parents:
41911
diff
changeset

76 
"Set_Algebras" 
24478  77 
]; 
21256  78 

41914
4ef7e6e317fa
only testing theory LSC_Examples when GHC is installed on the machine
bulwahn
parents:
41911
diff
changeset

79 
if getenv "EXEC_GHC" = "" then () 
4ef7e6e317fa
only testing theory LSC_Examples when GHC is installed on the machine
bulwahn
parents:
41911
diff
changeset

80 
else use_thy "LSC_Examples"; 
4ef7e6e317fa
only testing theory LSC_Examples when GHC is installed on the machine
bulwahn
parents:
41911
diff
changeset

81 

29376  82 
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

83 
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

84 
else use_thy "svc_test"; 
29376  85 

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

86 
(*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

87 
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

88 
else use_thy "Sudoku"; 
18408  89 

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

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

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

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