src/HOL/ex/ROOT.ML
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 30179 c703c9368c12
child 30374 7311a1546d85
permissions -rw-r--r--
added lemmas
     1 (*  Title:      HOL/ex/ROOT.ML
     2 
     3 Miscellaneous examples for Higher-Order Logic.
     4 *)
     5 
     6 no_document use_thys [
     7   "State_Monad",
     8   "Efficient_Nat_examples",
     9   "ExecutableContent",
    10   "FuncSet",
    11   "Word",
    12   "Eval_Examples",
    13   "Quickcheck_Generators",
    14   "Term_Of_Syntax",
    15   "Codegenerator",
    16   "Codegenerator_Pretty",
    17   "NormalForm",
    18   "../NumberTheory/Factorization"
    19 ];
    20 
    21 use_thys [
    22   "Numeral",
    23   "ImperativeQuicksort",
    24   "Higher_Order_Logic",
    25   "Abstract_NAT",
    26   "Guess",
    27   "Binary",
    28   "Recdefs",
    29   "Fundefs",
    30   "Induction_Scheme",
    31   "InductiveInvariant_examples",
    32   "LocaleTest2",
    33   "Records",
    34   "MonoidGroup",
    35   "BinEx",
    36   "Hex_Bin_Examples",
    37   "Antiquote",
    38   "Multiquote",
    39   "PER",
    40   "NatSum",
    41   "ThreeDivides",
    42   "Intuitionistic",
    43   "CTL",
    44   "Arith_Examples",
    45   "BT",
    46   "MergeSort",
    47   "Lagrange",
    48   "Groebner_Examples",
    49   "MT",
    50   "Unification",
    51   "Commutative_RingEx",
    52   "Commutative_Ring_Complete",
    53   "Primrec",
    54   "Tarski",
    55   "Adder",
    56   "Classical",
    57   "set",
    58   "Meson_Test",
    59   "Code_Antiq",
    60   "Termination",
    61   "Coherent",
    62   "Dense_Linear_Order_Ex",
    63   "PresburgerEx",
    64   "ReflectionEx",
    65   "BinEx",
    66   "Sqrt",
    67   "Sqrt_Script",
    68   "Arithmetic_Series_Complex",
    69   "HarmonicSeries",
    70   "Refute_Examples",
    71   "Quickcheck_Examples",
    72   "Formal_Power_Series_Examples"
    73 ];
    74 
    75 setmp Proofterm.proofs 2 use_thy "Hilbert_Classical";
    76 
    77 
    78 use_thy "SVC_Oracle";
    79 
    80 fun svc_enabled () = getenv "SVC_HOME" <> "";
    81 fun if_svc_enabled f x = if svc_enabled () then f x else ();
    82 
    83 if_svc_enabled use_thy "svc_test";
    84 
    85 
    86 (* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)
    87 (* installed:                                                       *)
    88 try use_thy "SAT_Examples";
    89 
    90 (* requires zChaff (or some other reasonably fast SAT solver) to be *)
    91 (* installed:                                                       *)
    92 if getenv "ZCHAFF_HOME" <> "" then
    93   use_thy "Sudoku"
    94 else ();
    95 
    96 HTML.with_charset "utf-8" (no_document use_thys)
    97   ["Hebrew", "Chinese", "Serbian"];