src/HOL/ex/ROOT.ML
changeset 11586 d8a7f6318457
parent 11445 01ee48a80800
child 12080 4c1e3a2a87c3
     1.1 --- a/src/HOL/ex/ROOT.ML	Thu Sep 27 15:42:01 2001 +0200
     1.2 +++ b/src/HOL/ex/ROOT.ML	Thu Sep 27 15:42:08 2001 +0200
     1.3 @@ -8,6 +8,20 @@
     1.4  time_use_thy "Recdefs";
     1.5  time_use_thy "Primrec";
     1.6  
     1.7 +setmp proofs 2 time_use_thy "Hilbert_Classical";
     1.8 +
     1.9 +(*advanced concrete syntax*)
    1.10 +time_use_thy "Tuple";
    1.11 +time_use_thy "Antiquote";
    1.12 +time_use_thy "Multiquote";
    1.13 +
    1.14 +(*basic use of extensible records*)
    1.15 +time_use_thy "MonoidGroup";
    1.16 +time_use_thy "Records";
    1.17 +
    1.18 +time_use_thy "StringEx";
    1.19 +time_use_thy "BinEx";
    1.20 +
    1.21  time_use_thy "NatSum";
    1.22  time_use     "cla.ML";
    1.23  time_use     "mesontest.ML";
    1.24 @@ -24,16 +38,4 @@
    1.25  time_use_thy "MT";
    1.26  time_use_thy "Tarski";
    1.27  
    1.28 -time_use_thy "StringEx";
    1.29 -time_use_thy "BinEx";
    1.30 -
    1.31  if_svc_enabled time_use_thy "svc_test";
    1.32 -
    1.33 -(*basic use of extensible records*)
    1.34 -time_use_thy "MonoidGroup";
    1.35 -time_use_thy "Records";
    1.36 -
    1.37 -(*advanced concrete syntax*)
    1.38 -time_use_thy "Tuple";
    1.39 -time_use_thy "Antiquote";
    1.40 -time_use_thy "Multiquote";