src/HOL/ex/ROOT.ML
author haftmann
Wed Aug 30 08:34:45 2006 +0200 (2006-08-30)
changeset 20436 0af8655ab0bb
parent 20427 0b102b4182de
child 20597 65fe827aa595
permissions -rw-r--r--
added yet another code generator example
     1 (*  Title:      HOL/ex/ROOT.ML
     2     ID:         $Id$
     3 
     4 Miscellaneous examples for Higher-Order Logic.
     5 *)
     6 
     7 no_document time_use_thy "Classpackage";
     8 no_document time_use_thy "Codegenerator";
     9 no_document time_use_thy "CodeOperationalEquality";
    10 no_document time_use_thy "CodeCollections";
    11 no_document time_use_thy "CodeEval";
    12 no_document time_use_thy "CodeRandom";
    13 
    14 time_use_thy "Higher_Order_Logic";
    15 time_use_thy "Abstract_NAT";
    16 time_use_thy "Guess";
    17 
    18 time_use_thy "Recdefs";
    19 time_use_thy "InductiveInvariant_examples";
    20 time_use_thy "Primrec";
    21 time_use_thy "Locales";
    22 time_use_thy "Records";
    23 time_use_thy "MonoidGroup";
    24 time_use_thy "StringEx";
    25 time_use_thy "BinEx";
    26 setmp proofs 2 time_use_thy "Hilbert_Classical";
    27 time_use_thy "Antiquote";
    28 time_use_thy "Multiquote";
    29 
    30 time_use_thy "NatSum";
    31 time_use_thy "ThreeDivides";
    32 time_use_thy "Intuitionistic";
    33 time_use_thy "Classical";
    34 time_use_thy "CTL";
    35 time_use_thy "mesontest2";
    36 time_use_thy "PresburgerEx";
    37 time_use_thy "Reflected_Presburger";
    38 time_use_thy "BT";
    39 time_use_thy "InSort";
    40 time_use_thy "Qsort";
    41 time_use_thy "MergeSort";
    42 time_use_thy "Puzzle";
    43 
    44 time_use_thy "Lagrange";
    45 time_use_thy "Commutative_RingEx";
    46 time_use_thy "Commutative_Ring_Complete";
    47 time_use_thy "Reflection";
    48 
    49 time_use_thy "set";
    50 time_use_thy "MT";
    51 
    52 no_document use_thy "FuncSet";
    53 time_use_thy "Tarski";
    54 
    55 time_use_thy "SVC_Oracle";
    56 if_svc_enabled time_use_thy "svc_test";
    57 
    58 (* requires zChaff with proof generation to be installed: *)
    59 try time_use_thy "SAT_Examples";
    60 
    61 (* requires zChaff (or some other reasonably fast SAT solver) to be installed: *)
    62 if getenv "ZCHAFF_HOME" <> "" then
    63   time_use_thy "Sudoku"
    64 else
    65   ();
    66 
    67 time_use_thy "Refute_Examples";
    68 time_use_thy "Quickcheck_Examples";
    69 no_document time_use_thy "NormalForm";
    70 
    71 no_document use_thy "Word";
    72 time_use_thy "Adder";
    73 
    74 HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew";
    75 HTML.with_charset "utf-8" (no_document time_use_thy) "Chinese";