back to normal;
authorwenzelm
Fri Nov 09 00:11:52 2001 +0100 (2001-11-09)
changeset 12115d0d41884f787
parent 12114 a8e860c86252
child 12116 4027b15377a5
back to normal;
tuned;
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/ex/ROOT.ML	Fri Nov 09 00:09:47 2001 +0100
     1.2 +++ b/src/HOL/ex/ROOT.ML	Fri Nov 09 00:11:52 2001 +0100
     1.3 @@ -1,2 +1,35 @@
     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 +time_use_thy "Recdefs";
    1.11 +time_use_thy "Primrec";
    1.12  time_use_thy "Locales";
    1.13 +time_use_thy "Records";
    1.14 +time_use_thy "MonoidGroup";
    1.15 +time_use_thy "StringEx";
    1.16 +time_use_thy "BinEx";
    1.17 +setmp proofs 2 time_use_thy "Hilbert_Classical";
    1.18 +time_use_thy "Antiquote";
    1.19 +time_use_thy "Multiquote";
    1.20 +time_use_thy "Tuple";
    1.21 +
    1.22 +time_use_thy "NatSum";
    1.23 +time_use     "cla.ML";
    1.24 +time_use     "mesontest.ML";
    1.25 +time_use_thy "mesontest2";
    1.26 +time_use_thy "BT";
    1.27 +time_use_thy "AVL";
    1.28 +time_use_thy "InSort";
    1.29 +time_use_thy "Qsort";
    1.30 +time_use_thy "Puzzle";
    1.31 +
    1.32 +time_use_thy "IntRing";
    1.33 +
    1.34 +time_use_thy "set";
    1.35 +time_use_thy "MT";
    1.36 +time_use_thy "Tarski";
    1.37 +
    1.38 +if_svc_enabled time_use_thy "svc_test";