src/HOL/ex/ROOT.ML
author huffman
Sun Mar 25 20:15:39 2012 +0200 (2012-03-25 ago)
changeset 47108 2a1953f0d20d
parent 46585 f462e49eaf11
child 47223 4fc34c628474
permissions -rw-r--r--
merged fork with new numeral representation (see NEWS)
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",
huffman@47108
     8
  "Code_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",
blanchet@43804
    14
  "Serbian"
haftmann@25963
    15
];
haftmann@25963
    16
wenzelm@24478
    17
use_thys [
wenzelm@40239
    18
  "Iff_Oracle",
wenzelm@40281
    19
  "Coercion_Examples",
huffman@46558
    20
  "Numeral_Representation",
wenzelm@24478
    21
  "Higher_Order_Logic",
wenzelm@24478
    22
  "Abstract_NAT",
wenzelm@24478
    23
  "Guess",
wenzelm@24478
    24
  "Binary",
wenzelm@24478
    25
  "Fundefs",
krauss@33471
    26
  "Induction_Schema",
wenzelm@24478
    27
  "LocaleTest2",
wenzelm@24478
    28
  "Records",
krauss@37760
    29
  "While_Combinator_Example",
wenzelm@24478
    30
  "MonoidGroup",
wenzelm@24478
    31
  "BinEx",
wenzelm@24478
    32
  "Hex_Bin_Examples",
wenzelm@24478
    33
  "Antiquote",
wenzelm@24478
    34
  "Multiquote",
wenzelm@24478
    35
  "PER",
wenzelm@24478
    36
  "NatSum",
wenzelm@24478
    37
  "ThreeDivides",
wenzelm@24478
    38
  "Intuitionistic",
wenzelm@24478
    39
  "CTL",
wenzelm@24478
    40
  "Arith_Examples",
wenzelm@24478
    41
  "BT",
nipkow@33436
    42
  "Tree23",
wenzelm@24478
    43
  "MergeSort",
wenzelm@24478
    44
  "Lagrange",
wenzelm@24478
    45
  "Groebner_Examples",
wenzelm@24478
    46
  "MT",
wenzelm@24478
    47
  "Unification",
wenzelm@24740
    48
  "Primrec",
wenzelm@24740
    49
  "Tarski",
wenzelm@25738
    50
  "Classical",
haftmann@44276
    51
  "Set_Theory",
haftmann@27436
    52
  "Meson_Test",
krauss@29181
    53
  "Termination",
wenzelm@29376
    54
  "Coherent",
wenzelm@29376
    55
  "PresburgerEx",
wenzelm@29377
    56
  "ReflectionEx",
wenzelm@29377
    57
  "Sqrt",
wenzelm@29377
    58
  "Sqrt_Script",
haftmann@32560
    59
  "Transfer_Ex",
wenzelm@29377
    60
  "Arithmetic_Series_Complex",
wenzelm@29377
    61
  "HarmonicSeries",
wenzelm@29377
    62
  "Refute_Examples",
haftmann@35160
    63
  "Landau",
haftmann@35163
    64
  "Execute_Choice",
hoelzl@35328
    65
  "Summation",
huffman@36793
    66
  "Gauge_Integration",
haftmann@40349
    67
  "Dedekind_Real",
bulwahn@40632
    68
  "Quicksort",
bulwahn@43238
    69
  "Birthday_Paradox",
haftmann@41582
    70
  "List_to_Set_Comprehension_Examples",
wenzelm@44962
    71
  "Set_Algebras",
huffman@45224
    72
  "Seq",
bulwahn@46395
    73
  "Simproc_Tests",
bulwahn@46395
    74
  "Executable_Relation"
wenzelm@24478
    75
];
wenzelm@21256
    76
wenzelm@29376
    77
use_thy "SVC_Oracle";
wenzelm@32428
    78
if getenv "SVC_HOME" = "" then ()
wenzelm@32428
    79
else use_thy "svc_test";
wenzelm@29376
    80
wenzelm@32428
    81
(*requires zChaff (or some other reasonably fast SAT solver)*)
wenzelm@32428
    82
if getenv "ZCHAFF_HOME" = "" then ()
wenzelm@32428
    83
else use_thy "Sudoku";
webertj@18408
    84
wenzelm@33546
    85
(*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
wenzelm@33546
    86
(*global side-effects ahead!*)
wenzelm@33546
    87
try use_thy "SAT_Examples";   (* FIXME try!? (not really a proper test) *)