src/HOL/ex/ROOT.ML
author haftmann
Mon Mar 23 19:01:17 2009 +0100 (2009-03-23 ago)
changeset 30689 b14b2cc4e25e
parent 30429 39acdf031548
child 30740 2d3ae5a7edb2
permissions -rw-r--r--
moved Imperative_HOL examples to Imperative_HOL/ex
wenzelm@12115
     1
(*  Title:      HOL/ex/ROOT.ML
wenzelm@11586
     2
wenzelm@12115
     3
Miscellaneous examples for Higher-Order Logic.
wenzelm@12115
     4
*)
wenzelm@12115
     5
wenzelm@24528
     6
no_document use_thys [
wenzelm@24740
     7
  "State_Monad",
haftmann@25963
     8
  "Efficient_Nat_examples",
haftmann@25963
     9
  "ExecutableContent",
haftmann@25963
    10
  "FuncSet",
haftmann@25963
    11
  "Word",
haftmann@25963
    12
  "Eval_Examples",
haftmann@29808
    13
  "Quickcheck_Generators",
wenzelm@29376
    14
  "Term_Of_Syntax",
wenzelm@29376
    15
  "Codegenerator",
wenzelm@29376
    16
  "Codegenerator_Pretty",
wenzelm@29377
    17
  "NormalForm",
haftmann@30374
    18
  "../NumberTheory/Factorization",
haftmann@30374
    19
  "Predicate_Compile"
haftmann@25963
    20
];
haftmann@25963
    21
wenzelm@24478
    22
use_thys [
haftmann@28021
    23
  "Numeral",
wenzelm@24478
    24
  "Higher_Order_Logic",
wenzelm@24478
    25
  "Abstract_NAT",
wenzelm@24478
    26
  "Guess",
wenzelm@24478
    27
  "Binary",
wenzelm@24478
    28
  "Recdefs",
wenzelm@24478
    29
  "Fundefs",
krauss@25568
    30
  "Induction_Scheme",
wenzelm@24478
    31
  "InductiveInvariant_examples",
wenzelm@24478
    32
  "LocaleTest2",
wenzelm@24478
    33
  "Records",
wenzelm@24478
    34
  "MonoidGroup",
wenzelm@24478
    35
  "BinEx",
wenzelm@24478
    36
  "Hex_Bin_Examples",
wenzelm@24478
    37
  "Antiquote",
wenzelm@24478
    38
  "Multiquote",
wenzelm@24478
    39
  "PER",
wenzelm@24478
    40
  "NatSum",
wenzelm@24478
    41
  "ThreeDivides",
wenzelm@24478
    42
  "Intuitionistic",
wenzelm@24478
    43
  "CTL",
wenzelm@24478
    44
  "Arith_Examples",
wenzelm@24478
    45
  "BT",
wenzelm@24478
    46
  "MergeSort",
wenzelm@24478
    47
  "Lagrange",
wenzelm@24478
    48
  "Groebner_Examples",
wenzelm@24478
    49
  "MT",
wenzelm@24478
    50
  "Unification",
wenzelm@24478
    51
  "Commutative_RingEx",
wenzelm@24740
    52
  "Commutative_Ring_Complete",
wenzelm@24740
    53
  "Primrec",
wenzelm@24740
    54
  "Tarski",
wenzelm@25738
    55
  "Adder",
wenzelm@25738
    56
  "Classical",
wenzelm@25738
    57
  "set",
haftmann@27436
    58
  "Meson_Test",
krauss@27742
    59
  "Code_Antiq",
krauss@29181
    60
  "Termination",
wenzelm@29376
    61
  "Coherent",
wenzelm@29376
    62
  "PresburgerEx",
wenzelm@29377
    63
  "ReflectionEx",
wenzelm@29377
    64
  "BinEx",
wenzelm@29377
    65
  "Sqrt",
wenzelm@29377
    66
  "Sqrt_Script",
wenzelm@29377
    67
  "Arithmetic_Series_Complex",
wenzelm@29377
    68
  "HarmonicSeries",
wenzelm@29377
    69
  "Refute_Examples",
chaieb@29697
    70
  "Quickcheck_Examples",
chaieb@29697
    71
  "Formal_Power_Series_Examples"
wenzelm@24478
    72
];
wenzelm@21256
    73
wenzelm@29376
    74
setmp Proofterm.proofs 2 use_thy "Hilbert_Classical";
wenzelm@24478
    75
wenzelm@12115
    76
wenzelm@29376
    77
use_thy "SVC_Oracle";
wenzelm@12115
    78
wenzelm@28263
    79
fun svc_enabled () = getenv "SVC_HOME" <> "";
wenzelm@28263
    80
fun if_svc_enabled f x = if svc_enabled () then f x else ();
wenzelm@28263
    81
wenzelm@29377
    82
if_svc_enabled use_thy "svc_test";
webertj@14459
    83
wenzelm@29376
    84
webertj@23191
    85
(* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)
webertj@23191
    86
(* installed:                                                       *)
wenzelm@29376
    87
try use_thy "SAT_Examples";
webertj@17618
    88
webertj@23191
    89
(* requires zChaff (or some other reasonably fast SAT solver) to be *)
webertj@23191
    90
(* installed:                                                       *)
webertj@18408
    91
if getenv "ZCHAFF_HOME" <> "" then
wenzelm@29376
    92
  use_thy "Sudoku"
webertj@23191
    93
else ();
webertj@18408
    94
wenzelm@30179
    95
HTML.with_charset "utf-8" (no_document use_thys)
wenzelm@30179
    96
  ["Hebrew", "Chinese", "Serbian"];