src/HOL/ex/ROOT.ML
author huffman
Fri Mar 30 14:27:29 2012 +0200 (2012-03-30 ago)
changeset 47223 4fc34c628474
parent 47108 2a1953f0d20d
child 47474 214bfaae738d
permissions -rw-r--r--
remove content-free theory ex/Arithmetic_Series_Complex.thy
     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   "HarmonicSeries",
    61   "Refute_Examples",
    62   "Landau",
    63   "Execute_Choice",
    64   "Summation",
    65   "Gauge_Integration",
    66   "Dedekind_Real",
    67   "Quicksort",
    68   "Birthday_Paradox",
    69   "List_to_Set_Comprehension_Examples",
    70   "Set_Algebras",
    71   "Seq",
    72   "Simproc_Tests",
    73   "Executable_Relation"
    74 ];
    75 
    76 use_thy "SVC_Oracle";
    77 if getenv "SVC_HOME" = "" then ()
    78 else use_thy "svc_test";
    79 
    80 (*requires zChaff (or some other reasonably fast SAT solver)*)
    81 if getenv "ZCHAFF_HOME" = "" then ()
    82 else use_thy "Sudoku";
    83 
    84 (*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
    85 (*global side-effects ahead!*)
    86 try use_thy "SAT_Examples";   (* FIXME try!? (not really a proper test) *)