src/HOL/ex/ROOT.ML
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 30179 c703c9368c12
child 30374 7311a1546d85
permissions -rw-r--r--
added lemmas
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@29788
    18
  "../NumberTheory/Factorization"
haftmann@25963
    19
];
haftmann@25963
    20
wenzelm@24478
    21
use_thys [
haftmann@28021
    22
  "Numeral",
haftmann@27679
    23
  "ImperativeQuicksort",
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
  "Dense_Linear_Order_Ex",
wenzelm@29376
    63
  "PresburgerEx",
wenzelm@29377
    64
  "ReflectionEx",
wenzelm@29377
    65
  "BinEx",
wenzelm@29377
    66
  "Sqrt",
wenzelm@29377
    67
  "Sqrt_Script",
wenzelm@29377
    68
  "Arithmetic_Series_Complex",
wenzelm@29377
    69
  "HarmonicSeries",
wenzelm@29377
    70
  "Refute_Examples",
chaieb@29697
    71
  "Quickcheck_Examples",
chaieb@29697
    72
  "Formal_Power_Series_Examples"
wenzelm@24478
    73
];
wenzelm@21256
    74
wenzelm@29376
    75
setmp Proofterm.proofs 2 use_thy "Hilbert_Classical";
wenzelm@24478
    76
wenzelm@12115
    77
wenzelm@29376
    78
use_thy "SVC_Oracle";
wenzelm@12115
    79
wenzelm@28263
    80
fun svc_enabled () = getenv "SVC_HOME" <> "";
wenzelm@28263
    81
fun if_svc_enabled f x = if svc_enabled () then f x else ();
wenzelm@28263
    82
wenzelm@29377
    83
if_svc_enabled use_thy "svc_test";
webertj@14459
    84
wenzelm@29376
    85
webertj@23191
    86
(* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)
webertj@23191
    87
(* installed:                                                       *)
wenzelm@29376
    88
try use_thy "SAT_Examples";
webertj@17618
    89
webertj@23191
    90
(* requires zChaff (or some other reasonably fast SAT solver) to be *)
webertj@23191
    91
(* installed:                                                       *)
webertj@18408
    92
if getenv "ZCHAFF_HOME" <> "" then
wenzelm@29376
    93
  use_thy "Sudoku"
webertj@23191
    94
else ();
webertj@18408
    95
wenzelm@30179
    96
HTML.with_charset "utf-8" (no_document use_thys)
wenzelm@30179
    97
  ["Hebrew", "Chinese", "Serbian"];