author  krauss 
Sat, 27 Dec 2008 17:35:00 +0100  
changeset 29181  cc177742e607 
parent 28952  15a4b2cf8c34 
child 29376  2071939cf0fc 
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", 
14 
"Term_Of_Syntax" 

25963  15 
]; 
16 

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

17 
no_document use_thy "Codegenerator"; 
28353  18 
no_document use_thy "Codegenerator_Pretty"; 
24478  19 

20 
use_thys [ 

28021  21 
"Numeral", 
27679  22 
"ImperativeQuicksort", 
24478  23 
"Higher_Order_Logic", 
24 
"Abstract_NAT", 

25 
"Guess", 

26 
"Binary", 

27 
"Recdefs", 

28 
"Fundefs", 

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

32 
"Records", 

33 
"MonoidGroup", 

34 
"BinEx", 

35 
"Hex_Bin_Examples", 

36 
"Antiquote", 

37 
"Multiquote", 

38 
"PER", 

39 
"NatSum", 

40 
"ThreeDivides", 

41 
"Intuitionistic", 

42 
"CTL", 

43 
"Arith_Examples", 

44 
"BT", 

45 
"MergeSort", 

46 
"Lagrange", 

47 
"Groebner_Examples", 

48 
"MT", 

49 
"Unification", 

50 
"Commutative_RingEx", 

24740  51 
"Commutative_Ring_Complete", 
52 
"Primrec", 

53 
"Tarski", 

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

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

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

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

59 
"Termination", 
28324  60 
"Coherent" 
24478  61 
]; 
21256  62 

25374  63 
setmp Proofterm.proofs 2 time_use_thy "Hilbert_Classical"; 
24478  64 

23454
c54975167be9
replaced Real/FerranteRackoff tool by generic version in Main HOL;
wenzelm
parents:
23302
diff
changeset

65 
time_use_thy "Dense_Linear_Order_Ex"; 
13880  66 
time_use_thy "PresburgerEx"; 
23808  67 
time_use_thy "Reflected_Presburger"; 
12115  68 

28866
30cd9d89a0fb
reactivated some dead theories (based on hints by Mark Hillebrand);
wenzelm
parents:
28630
diff
changeset

69 
use_thys ["Reflection", "ReflectionEx"]; 
12115  70 

12869  71 
time_use_thy "SVC_Oracle"; 
28263  72 

73 
(*check if user has SVC installed*) 

74 
fun svc_enabled () = getenv "SVC_HOME" <> ""; 

75 
fun if_svc_enabled f x = if svc_enabled () then f x else (); 

76 

12115  77 
if_svc_enabled time_use_thy "svc_test"; 
14459  78 

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

18678  81 
try time_use_thy "SAT_Examples"; 
17618
1330157e156a
new sat tactic imports resolution proofs from zChaff
webertj
parents:
17505
diff
changeset

82 

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

18408  85 
if getenv "ZCHAFF_HOME" <> "" then 
86 
time_use_thy "Sudoku" 

23191  87 
else (); 
18408  88 

14462  89 
time_use_thy "Refute_Examples"; 
14592
dd1a2905ea73
Added theory with examples for quickcheck command.
berghofe
parents:
14569
diff
changeset

90 
time_use_thy "Quickcheck_Examples"; 
19832  91 
no_document time_use_thy "NormalForm"; 
14494
48ae8d678d88
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
14482
diff
changeset

92 

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

93 
HTML.with_charset "utf8" (no_document use_thys) ["Hebrew", "Chinese"]; 
bcb1e9b7644b
Codegenerator vs. Codegenerator_Pretty: loaded sequentially, due to hazardous ML sections;
wenzelm
parents:
25963
diff
changeset

94 

27421  95 
no_document use_thys [ 
96 
"../NumberTheory/Factorization", 

28098  97 
"../Library/BigO" 
27421  98 
]; 
99 

100 
use_thys [ 

28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28866
diff
changeset

101 
"BinEx", 
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28866
diff
changeset

102 
"Sqrt", 
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28866
diff
changeset

103 
"Sqrt_Script", 
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28866
diff
changeset

104 
"BigO_Complex", 
27421  105 

28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28866
diff
changeset

106 
"Arithmetic_Series_Complex", 
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28866
diff
changeset

107 
"HarmonicSeries", 
27421  108 

28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28866
diff
changeset

109 
"MIR", 
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28866
diff
changeset

110 
"ReflectedFerrack" 
27421  111 
]; 
112 