src/HOL/ex/ROOT.ML
author haftmann
Wed Mar 12 19:38:14 2008 +0100 (2008-03-12)
changeset 26265 4b63b9e9b10d
parent 26104 200b4e401e65
child 27421 7e458bd56860
permissions -rw-r--r--
separated Random.thy from Quickcheck.thy
     1 (*  Title:      HOL/ex/ROOT.ML
     2     ID:         $Id$
     3 
     4 Miscellaneous examples for Higher-Order Logic.
     5 *)
     6 
     7 no_document use_thys [
     8   "Parity",
     9   "GCD",
    10   "Eval",
    11   "State_Monad",
    12   "Efficient_Nat_examples",
    13   "ExecutableContent",
    14   "FuncSet",
    15   "Word",
    16   "Eval_Examples",
    17   "Quickcheck"
    18 ];
    19 
    20 no_document use_thy "Codegenerator";
    21 no_document use_thy "Codegenerator_Pretty";
    22 
    23 use_thys [
    24   "Higher_Order_Logic",
    25   "Abstract_NAT",
    26   "Guess",
    27   "Binary",
    28   "Recdefs",
    29   "Fundefs",
    30   "Induction_Scheme",
    31   "InductiveInvariant_examples",
    32   "Locales",
    33   "LocaleTest2",
    34   "Records",
    35   "MonoidGroup",
    36   "BinEx",
    37   "Hex_Bin_Examples",
    38   "Antiquote",
    39   "Multiquote",
    40   "PER",
    41   "NatSum",
    42   "ThreeDivides",
    43   "Intuitionistic",
    44   "CTL",
    45   "Arith_Examples",
    46   "BT",
    47   "MergeSort",
    48   "Puzzle",
    49   "Lagrange",
    50   "Groebner_Examples",
    51   "MT",
    52   "Unification",
    53   "Commutative_RingEx",
    54   "Commutative_Ring_Complete",
    55   "Primrec",
    56   "Tarski",
    57   "Adder",
    58   "Classical",
    59   "set",
    60   "Meson_Test"
    61 ];
    62 
    63 setmp Proofterm.proofs 2 time_use_thy "Hilbert_Classical";
    64 
    65 time_use_thy "Dense_Linear_Order_Ex";
    66 time_use_thy "PresburgerEx";
    67 time_use_thy "Reflected_Presburger";
    68 
    69 time_use_thy "Reflection";
    70 
    71 time_use_thy "SVC_Oracle";
    72 if_svc_enabled time_use_thy "svc_test";
    73 
    74 (* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)
    75 (* installed:                                                       *)
    76 try time_use_thy "SAT_Examples";
    77 
    78 (* requires zChaff (or some other reasonably fast SAT solver) to be *)
    79 (* installed:                                                       *)
    80 if getenv "ZCHAFF_HOME" <> "" then
    81   time_use_thy "Sudoku"
    82 else ();
    83 
    84 time_use_thy "Refute_Examples";
    85 time_use_thy "Quickcheck_Examples";
    86 no_document time_use_thy "NormalForm";
    87 
    88 HTML.with_charset "utf-8" (no_document use_thys) ["Hebrew", "Chinese"];
    89