Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/HOL/ex/ROOT.ML
author haftmann
Thu, 09 Aug 2007 15:52:45 +0200
changeset 24195 7d1a16c77f7c
parent 24127 a56b6ed2e49c
child 24478 fb5e3fcfc10c
permissions -rw-r--r--
tuned 
     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 

    12 no_document time_use_thy "Eval";

    13 time_use_thy "Eval_Examples";

    14 

    15 no_document time_use_thy "State_Monad";

    16 no_document time_use_thy "Pretty_Int";

    17 time_use_thy "Random";

    18 

    19 no_document time_use_thy "Executable_Rat";

    20 no_document time_use_thy "Efficient_Nat";

    21 no_document time_use_thy "Codegenerator";

    22 no_document time_use_thy "Codegenerator_Pretty";

    23 

    24 time_use_thy "Higher_Order_Logic";

    25 time_use_thy "Abstract_NAT";

    26 time_use_thy "Guess";

    27 time_use_thy "Binary";

    28 

    29 time_use_thy "Recdefs";

    30 time_use_thy "Fundefs";

    31 time_use_thy "InductiveInvariant_examples";

    32 time_use_thy "Primrec";

    33 time_use_thy "Locales";

    34 time_use_thy "LocaleTest2";

    35 time_use_thy "Records";

    36 time_use_thy "MonoidGroup";

    37 time_use_thy "BinEx";

    38 time_use_thy "Hex_Bin_Examples";

    39 setmp proofs 2 time_use_thy "Hilbert_Classical";

    40 time_use_thy "Antiquote";

    41 time_use_thy "Multiquote";

    42 

    43 time_use_thy "PER";

    44 time_use_thy "NatSum";

    45 time_use_thy "ThreeDivides";

    46 time_use_thy "Intuitionistic";

    47 time_use_thy "Classical";

    48 time_use_thy "CTL";

    49 time_use_thy "Meson_Test";

    50 time_use_thy "Arith_Examples";

    51 time_use_thy "Dense_Linear_Order_Ex";

    52 time_use_thy "PresburgerEx";

    53 time_use_thy "Reflected_Presburger";

    54 time_use_thy "BT";

    55 time_use_thy "InSort";

    56 time_use_thy "Qsort";

    57 time_use_thy "MergeSort";

    58 time_use_thy "Puzzle";

    59 

    60 time_use_thy "Lagrange";

    61 time_use_thy "Groebner_Examples";

    62 

    63 time_use_thy "Commutative_RingEx";

    64 time_use_thy "Commutative_Ring_Complete";

    65 time_use_thy "Reflection";

    66 

    67 time_use_thy "NBE";

    68 

    69 time_use_thy "set";

    70 time_use_thy "MT";

    71 

    72 no_document use_thy "FuncSet";

    73 time_use_thy "Tarski";

    74 

    75 time_use_thy "SVC_Oracle";

    76 if_svc_enabled time_use_thy "svc_test";

    77 

    78 (* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)

    79 (* installed:                                                       *)

    80 try time_use_thy "SAT_Examples";

    81 

    82 (* requires zChaff (or some other reasonably fast SAT solver) to be *)

    83 (* installed:                                                       *)

    84 if getenv "ZCHAFF_HOME" <> "" then

    85   time_use_thy "Sudoku"

    86 else ();

    87 

    88 time_use_thy "Refute_Examples";

    89 time_use_thy "Quickcheck_Examples";

    90 no_document time_use_thy "NormalForm";

    91 

    92 no_document use_thy "Word";

    93 time_use_thy "Adder";

    94 

    95 HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew";

    96 HTML.with_charset "utf-8" (no_document time_use_thy) "Chinese";

    97 

    98 time_use_thy "Unification";
wneuper/isa