src/HOL/ex/ROOT.ML
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45224 b1d5b3820d82
child 46395 f56be74d7f51
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
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",
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",
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
  "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",
chaieb@29697
    63
  "Quickcheck_Examples",
bulwahn@37917
    64
  "Quickcheck_Lattice_Examples",
haftmann@35160
    65
  "Landau",
haftmann@35163
    66
  "Execute_Choice",
hoelzl@35328
    67
  "Summation",
huffman@36793
    68
  "Gauge_Integration",
haftmann@40349
    69
  "Dedekind_Real",
bulwahn@40632
    70
  "Quicksort",
bulwahn@43238
    71
  "Birthday_Paradox",
haftmann@41582
    72
  "List_to_Set_Comprehension_Examples",
wenzelm@44962
    73
  "Set_Algebras",
huffman@45224
    74
  "Seq",
huffman@45224
    75
  "Simproc_Tests"
wenzelm@24478
    76
];
wenzelm@21256
    77
wenzelm@41952
    78
if getenv "ISABELLE_GHC" = "" then ()
bulwahn@41932
    79
else use_thy "Quickcheck_Narrowing_Examples";
bulwahn@41914
    80
wenzelm@29376
    81
use_thy "SVC_Oracle";
wenzelm@32428
    82
if getenv "SVC_HOME" = "" then ()
wenzelm@32428
    83
else use_thy "svc_test";
wenzelm@29376
    84
wenzelm@32428
    85
(*requires zChaff (or some other reasonably fast SAT solver)*)
wenzelm@32428
    86
if getenv "ZCHAFF_HOME" = "" then ()
wenzelm@32428
    87
else use_thy "Sudoku";
webertj@18408
    88
wenzelm@33546
    89
(*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
wenzelm@33546
    90
(*global side-effects ahead!*)
wenzelm@33546
    91
try use_thy "SAT_Examples";   (* FIXME try!? (not really a proper test) *)