src/HOL/ex/ROOT.ML
author huffman
Fri Aug 19 14:17:28 2011 -0700 (2011-08-19)
changeset 44311 42c5cbf68052
parent 44276 fe769a0fcc96
child 44962 5554ed48b13f
permissions -rw-r--r--
Transcendental.thy: add tendsto_intros lemmas;
new isCont theorems;
simplify some proofs.
     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   "Efficient_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",
    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   "BinEx",
    58   "Sqrt",
    59   "Sqrt_Script",
    60   "Transfer_Ex",
    61   "Arithmetic_Series_Complex",
    62   "HarmonicSeries",
    63   "Refute_Examples",
    64   "Quickcheck_Examples",
    65   "Quickcheck_Lattice_Examples",
    66   "Landau",
    67   "Execute_Choice",
    68   "Summation",
    69   "Gauge_Integration",
    70   "Dedekind_Real",
    71   "Quicksort",
    72   "Birthday_Paradox",
    73   "List_to_Set_Comprehension_Examples",
    74   "Set_Algebras"
    75 ];
    76 
    77 if getenv "ISABELLE_GHC" = "" then ()
    78 else use_thy "Quickcheck_Narrowing_Examples";
    79 
    80 use_thy "SVC_Oracle";
    81 if getenv "SVC_HOME" = "" then ()
    82 else use_thy "svc_test";
    83 
    84 (*requires zChaff (or some other reasonably fast SAT solver)*)
    85 if getenv "ZCHAFF_HOME" = "" then ()
    86 else use_thy "Sudoku";
    87 
    88 (*requires a proof-generating SAT solver (zChaff or MiniSAT)*)
    89 (*global side-effects ahead!*)
    90 try use_thy "SAT_Examples";   (* FIXME try!? (not really a proper test) *)