src/HOL/ex/ROOT.ML
author blanchet
Wed Mar 23 10:06:27 2011 +0100 (2011-03-23)
changeset 42071 04577a7e0c51
parent 41952 c7297638599b
child 42078 d5bf0ce40bd7
permissions -rw-r--r--
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
default to "e" rather than "vampire" since E is part of the Isabelle bundle
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@41413
     7
  "~~/src/HOL/Library/State_Monad",
haftmann@25963
     8
  "Efficient_Nat_examples",
wenzelm@41413
     9
  "~~/src/HOL/Library/FuncSet",
haftmann@25963
    10
  "Eval_Examples",
wenzelm@40946
    11
  "Normalization_by_Evaluation",
wenzelm@40946
    12
  "Hebrew",
wenzelm@40946
    13
  "Chinese",
wenzelm@40946
    14
  "Serbian"
haftmann@25963
    15
];
haftmann@25963
    16
wenzelm@24478
    17
use_thys [
wenzelm@40239
    18
  "Iff_Oracle",
wenzelm@40281
    19
  "Coercion_Examples",
haftmann@28021
    20
  "Numeral",
wenzelm@24478
    21
  "Higher_Order_Logic",
wenzelm@24478
    22
  "Abstract_NAT",
wenzelm@24478
    23
  "Guess",
wenzelm@24478
    24
  "Binary",
wenzelm@24478
    25
  "Recdefs",
wenzelm@24478
    26
  "Fundefs",
krauss@33471
    27
  "Induction_Schema",
wenzelm@24478
    28
  "InductiveInvariant_examples",
wenzelm@24478
    29
  "LocaleTest2",
wenzelm@24478
    30
  "Records",
krauss@37760
    31
  "While_Combinator_Example",
wenzelm@24478
    32
  "MonoidGroup",
wenzelm@24478
    33
  "BinEx",
wenzelm@24478
    34
  "Hex_Bin_Examples",
wenzelm@24478
    35
  "Antiquote",
wenzelm@24478
    36
  "Multiquote",
wenzelm@24478
    37
  "PER",
wenzelm@24478
    38
  "NatSum",
wenzelm@24478
    39
  "ThreeDivides",
wenzelm@24478
    40
  "Intuitionistic",
wenzelm@24478
    41
  "CTL",
wenzelm@24478
    42
  "Arith_Examples",
wenzelm@24478
    43
  "BT",
nipkow@33436
    44
  "Tree23",
wenzelm@24478
    45
  "MergeSort",
wenzelm@24478
    46
  "Lagrange",
wenzelm@24478
    47
  "Groebner_Examples",
wenzelm@24478
    48
  "MT",
wenzelm@24478
    49
  "Unification",
wenzelm@24740
    50
  "Primrec",
wenzelm@24740
    51
  "Tarski",
wenzelm@25738
    52
  "Classical",
wenzelm@25738
    53
  "set",
haftmann@27436
    54
  "Meson_Test",
krauss@29181
    55
  "Termination",
wenzelm@29376
    56
  "Coherent",
wenzelm@29376
    57
  "PresburgerEx",
wenzelm@29377
    58
  "ReflectionEx",
wenzelm@29377
    59
  "BinEx",
wenzelm@29377
    60
  "Sqrt",
wenzelm@29377
    61
  "Sqrt_Script",
haftmann@32560
    62
  "Transfer_Ex",
wenzelm@29377
    63
  "Arithmetic_Series_Complex",
wenzelm@29377
    64
  "HarmonicSeries",
wenzelm@29377
    65
  "Refute_Examples",
chaieb@29697
    66
  "Quickcheck_Examples",
bulwahn@37917
    67
  "Quickcheck_Lattice_Examples",
haftmann@35160
    68
  "Landau",
haftmann@35163
    69
  "Execute_Choice",
hoelzl@35328
    70
  "Summation",
huffman@36793
    71
  "Gauge_Integration",
haftmann@40349
    72
  "Dedekind_Real",
bulwahn@40632
    73
  "Quicksort",
bulwahn@41465
    74
  "Birthday_Paradoxon",
haftmann@41582
    75
  "List_to_Set_Comprehension_Examples",
blanchet@42071
    76
  "Set_Algebras",
blanchet@42071
    77
  "TPTP"
wenzelm@24478
    78
];
wenzelm@21256
    79
wenzelm@41952
    80
if getenv "ISABELLE_GHC" = "" then ()
bulwahn@41932
    81
else use_thy "Quickcheck_Narrowing_Examples";
bulwahn@41914
    82
wenzelm@29376
    83
use_thy "SVC_Oracle";
wenzelm@32428
    84
if getenv "SVC_HOME" = "" then ()
wenzelm@32428
    85
else use_thy "svc_test";
wenzelm@29376
    86
wenzelm@32428
    87
(*requires zChaff (or some other reasonably fast SAT solver)*)
wenzelm@32428
    88
if getenv "ZCHAFF_HOME" = "" then ()
wenzelm@32428
    89
else use_thy "Sudoku";
webertj@18408
    90
wenzelm@33546
    91
(*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
wenzelm@33546
    92
(*global side-effects ahead!*)
wenzelm@33546
    93
try use_thy "SAT_Examples";   (* FIXME try!? (not really a proper test) *)