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)
     1 (*  Title:      HOL/ex/ROOT.ML
     2 
     3 Miscellaneous examples for Higher-Order Logic.
     4 *)
     5 
     6 no_document use_thys [
     7   "~~/src/HOL/Library/State_Monad",
     8   "Code_Nat_examples",
     9   "~~/src/HOL/Library/FuncSet",
    10   "Eval_Examples",
    11   "Normalization_by_Evaluation",
    12   "Hebrew",
    13   "Chinese",
    14   "Serbian"
    15 ];
    16 
    17 use_thys [
    18   "Iff_Oracle",
    19   "Coercion_Examples",
    20   "Numeral_Representation",
    21   "Higher_Order_Logic",
    22   "Abstract_NAT",
    23   "Guess",
    24   "Binary",
    25   "Fundefs",
    26   "Induction_Schema",
    27   "LocaleTest2",
    28   "Records",
    29   "While_Combinator_Example",
    30   "MonoidGroup",
    31   "BinEx",
    32   "Hex_Bin_Examples",
    33   "Antiquote",
    34   "Multiquote",
    35   "PER",
    36   "NatSum",
    37   "ThreeDivides",
    38   "Intuitionistic",
    39   "CTL",
    40   "Arith_Examples",
    41   "BT",
    42   "Tree23",
    43   "MergeSort",
    44   "Lagrange",
    45   "Groebner_Examples",
    46   "MT",
    47   "Unification",
    48   "Primrec",
    49   "Tarski",
    50   "Classical",
    51   "Set_Theory",
    52   "Meson_Test",
    53   "Termination",
    54   "Coherent",
    55   "PresburgerEx",
    56   "ReflectionEx",
    57   "Sqrt",
    58   "Sqrt_Script",
    59   "Transfer_Ex",
    60   "Arithmetic_Series_Complex",
    61   "HarmonicSeries",
    62   "Refute_Examples",
    63   "Landau",
    64   "Execute_Choice",
    65   "Summation",
    66   "Gauge_Integration",
    67   "Dedekind_Real",
    68   "Quicksort",
    69   "Birthday_Paradox",
    70   "List_to_Set_Comprehension_Examples",
    71   "Set_Algebras",
    72   "Seq",
    73   "Simproc_Tests",
    74   "Executable_Relation"
    75 ];
    76 
    77 use_thy "SVC_Oracle";
    78 if getenv "SVC_HOME" = "" then ()
    79 else use_thy "svc_test";
    80 
    81 (*requires zChaff (or some other reasonably fast SAT solver)*)
    82 if getenv "ZCHAFF_HOME" = "" then ()
    83 else use_thy "Sudoku";
    84 
    85 (*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
    86 (*global side-effects ahead!*)
    87 try use_thy "SAT_Examples";   (* FIXME try!? (not really a proper test) *)