src/HOL/ex/ROOT.ML
author webertj
Fri Jun 01 23:21:40 2007 +0200 (2007-06-01)
changeset 23193 1f2d94b6a8ef
parent 23191 b7f3a30f3d7f
child 23271 3f9ef4bf3f31
permissions -rw-r--r--
some tests for arith added
     1 (*  Title:      HOL/ex/ROOT.ML
     2     ID:         $Id$
     3 
     4 Miscellaneous examples for Higher-Order Logic.
     5 *)
     6 
     7 no_document use_thy "Parity";
     8 no_document use_thy "GCD";
     9 
    10 no_document time_use_thy "Classpackage";
    11 no_document time_use_thy "Eval_examples";
    12 no_document time_use_thy "Random";
    13 no_document time_use_thy "Codegenerator_Rat";
    14 no_document time_use_thy "Codegenerator";
    15 
    16 time_use_thy "Higher_Order_Logic";
    17 time_use_thy "Abstract_NAT";
    18 time_use_thy "Guess";
    19 time_use_thy "Binary";
    20 
    21 time_use_thy "Recdefs";
    22 time_use_thy "Fundefs";
    23 time_use_thy "InductiveInvariant_examples";
    24 time_use_thy "Primrec";
    25 time_use_thy "Locales";
    26 time_use_thy "LocaleTest2";
    27 time_use_thy "Records";
    28 time_use_thy "MonoidGroup";
    29 time_use_thy "BinEx";
    30 time_use_thy "Hex_Bin_Examples";
    31 setmp proofs 2 time_use_thy "Hilbert_Classical";
    32 time_use_thy "Antiquote";
    33 time_use_thy "Multiquote";
    34 
    35 time_use_thy "PER";
    36 time_use_thy "NatSum";
    37 time_use_thy "ThreeDivides";
    38 time_use_thy "Intuitionistic";
    39 time_use_thy "Classical";
    40 time_use_thy "CTL";
    41 time_use_thy "mesontest2";
    42 time_use_thy "Arith_Examples";
    43 time_use_thy "PresburgerEx";
    44 time_use_thy "Reflected_Presburger";
    45 time_use_thy "BT";
    46 time_use_thy "InSort";
    47 time_use_thy "Qsort";
    48 time_use_thy "MergeSort";
    49 time_use_thy "Puzzle";
    50 
    51 time_use_thy "Lagrange";
    52 time_use_thy "Commutative_RingEx";
    53 time_use_thy "Commutative_Ring_Complete";
    54 time_use_thy "Reflection";
    55 
    56 time_use_thy "set";
    57 time_use_thy "MT";
    58 
    59 no_document use_thy "FuncSet";
    60 time_use_thy "Tarski";
    61 
    62 time_use_thy "SVC_Oracle";
    63 if_svc_enabled time_use_thy "svc_test";
    64 
    65 (* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)
    66 (* installed:                                                       *)
    67 try time_use_thy "SAT_Examples";
    68 
    69 (* requires zChaff (or some other reasonably fast SAT solver) to be *)
    70 (* installed:                                                       *)
    71 if getenv "ZCHAFF_HOME" <> "" then
    72   time_use_thy "Sudoku"
    73 else ();
    74 
    75 time_use_thy "Refute_Examples";
    76 time_use_thy "Quickcheck_Examples";
    77 no_document time_use_thy "NormalForm";
    78 
    79 no_document use_thy "Word";
    80 time_use_thy "Adder";
    81 
    82 HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew";
    83 HTML.with_charset "utf-8" (no_document time_use_thy) "Chinese";
    84 
    85 time_use_thy "Unification";