src/HOL/ex/ROOT.ML
changeset 12105 1e4451999200
parent 12080 4c1e3a2a87c3
child 12115 d0d41884f787
     1.1 --- a/src/HOL/ex/ROOT.ML	Thu Nov 08 17:54:58 2001 +0100
     1.2 +++ b/src/HOL/ex/ROOT.ML	Thu Nov 08 23:50:08 2001 +0100
     1.3 @@ -1,42 +1,2 @@
     1.4 -(*  Title:      HOL/ex/ROOT.ML
     1.5 -    ID:         $Id$
     1.6 -
     1.7 -Miscellaneous examples for Higher-Order Logic.
     1.8 -*)
     1.9 -
    1.10 -(*some examples of recursive function definitions: the TFL package*)
    1.11 -time_use_thy "Recdefs";
    1.12 -time_use_thy "Primrec";
    1.13 -
    1.14 -setmp proofs 2 time_use_thy "Hilbert_Classical";
    1.15 -
    1.16 -(*advanced concrete syntax*)
    1.17 -time_use_thy "Tuple";
    1.18 -time_use_thy "Antiquote";
    1.19 -time_use_thy "Multiquote";
    1.20 -
    1.21 -(*basic use of extensible records*)
    1.22 -time_use_thy "MonoidGroup";
    1.23 -time_use_thy "Records";
    1.24  
    1.25  time_use_thy "Locales";
    1.26 -time_use_thy "StringEx";
    1.27 -time_use_thy "BinEx";
    1.28 -
    1.29 -time_use_thy "NatSum";
    1.30 -time_use     "cla.ML";
    1.31 -time_use     "mesontest.ML";
    1.32 -time_use_thy "mesontest2";
    1.33 -time_use_thy "BT";
    1.34 -time_use_thy "AVL";
    1.35 -time_use_thy "InSort";
    1.36 -time_use_thy "Qsort";
    1.37 -time_use_thy "Puzzle";
    1.38 -
    1.39 -time_use_thy "IntRing";
    1.40 -
    1.41 -time_use_thy "set";
    1.42 -time_use_thy "MT";
    1.43 -time_use_thy "Tarski";
    1.44 -
    1.45 -if_svc_enabled time_use_thy "svc_test";