1.1 --- a/src/HOL/ex/ROOT.ML	Wed Aug 29 19:00:40 2007 +0200
     1.2 +++ b/src/HOL/ex/ROOT.ML	Wed Aug 29 20:18:23 2007 +0200
     1.3 @@ -4,8 +4,45 @@
     1.4  Miscellaneous examples for Higher-Order Logic.
     1.5  *)
     1.6  
     1.7 -no_document use_thy "Parity";
     1.8 -no_document use_thy "GCD";
     1.9 +no_document use_thys  [
    1.10 +  "Parity",
    1.11 +  "GCD"
    1.12 +];
    1.13 +
    1.14 +use_thys [
    1.15 +  "Higher_Order_Logic",
    1.16 +  "Abstract_NAT",
    1.17 +  "Guess",
    1.18 +  "Binary",
    1.19 +  "Recdefs",
    1.20 +  "Fundefs",
    1.21 +  "InductiveInvariant_examples",
    1.22 +  "Locales",
    1.23 +  "LocaleTest2",
    1.24 +  "Records",
    1.25 +  "MonoidGroup",
    1.26 +  "BinEx",
    1.27 +  "Hex_Bin_Examples",
    1.28 +  "Antiquote",
    1.29 +  "Multiquote",
    1.30 +  "PER",
    1.31 +  "NatSum",
    1.32 +  "ThreeDivides",
    1.33 +  "Intuitionistic",
    1.34 +  "CTL",
    1.35 +  "Arith_Examples",
    1.36 +  "BT",
    1.37 +  "InSort",
    1.38 +  "Qsort",
    1.39 +  "MergeSort",
    1.40 +  "Puzzle",
    1.41 +  "Lagrange",
    1.42 +  "Groebner_Examples",
    1.43 +  "MT",
    1.44 +  "Unification",
    1.45 +  "Commutative_RingEx",
    1.46 +  "Commutative_Ring_Complete"
    1.47 +];
    1.48  
    1.49  no_document time_use_thy "Classpackage";
    1.50  
    1.51 @@ -21,54 +58,22 @@
    1.52  no_document time_use_thy "Codegenerator";
    1.53  no_document time_use_thy "Codegenerator_Pretty";
    1.54  
    1.55 -time_use_thy "Higher_Order_Logic";
    1.56 -time_use_thy "Abstract_NAT";
    1.57 -time_use_thy "Guess";
    1.58 -time_use_thy "Binary";
    1.59  
    1.60 -time_use_thy "Recdefs";
    1.61 -time_use_thy "Fundefs";
    1.62 -time_use_thy "InductiveInvariant_examples";
    1.63 +setmp proofs 2 time_use_thy "Hilbert_Classical";
    1.64 +
    1.65  time_use_thy "Primrec";
    1.66 -time_use_thy "Locales";
    1.67 -time_use_thy "LocaleTest2";
    1.68 -time_use_thy "Records";
    1.69 -time_use_thy "MonoidGroup";
    1.70 -time_use_thy "BinEx";
    1.71 -time_use_thy "Hex_Bin_Examples";
    1.72 -setmp proofs 2 time_use_thy "Hilbert_Classical";
    1.73 -time_use_thy "Antiquote";
    1.74 -time_use_thy "Multiquote";
    1.75 +time_use_thy "Classical";
    1.76 +time_use_thy "set";
    1.77  
    1.78 -time_use_thy "PER";
    1.79 -time_use_thy "NatSum";
    1.80 -time_use_thy "ThreeDivides";
    1.81 -time_use_thy "Intuitionistic";
    1.82 -time_use_thy "Classical";
    1.83 -time_use_thy "CTL";
    1.84  time_use_thy "Meson_Test";
    1.85 -time_use_thy "Arith_Examples";
    1.86  time_use_thy "Dense_Linear_Order_Ex";
    1.87  time_use_thy "PresburgerEx";
    1.88  time_use_thy "Reflected_Presburger";
    1.89 -time_use_thy "BT";
    1.90 -time_use_thy "InSort";
    1.91 -time_use_thy "Qsort";
    1.92 -time_use_thy "MergeSort";
    1.93 -time_use_thy "Puzzle";
    1.94  
    1.95 -time_use_thy "Lagrange";
    1.96 -time_use_thy "Groebner_Examples";
    1.97 -
    1.98 -time_use_thy "Commutative_RingEx";
    1.99 -time_use_thy "Commutative_Ring_Complete";
   1.100  time_use_thy "Reflection";
   1.101  
   1.102  time_use_thy "NBE";
   1.103  
   1.104 -time_use_thy "set";
   1.105 -time_use_thy "MT";
   1.106 -
   1.107  no_document use_thy "FuncSet";
   1.108  time_use_thy "Tarski";
   1.109  
   1.110 @@ -94,5 +99,3 @@
   1.111  
   1.112  HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew";
   1.113  HTML.with_charset "utf-8" (no_document time_use_thy) "Chinese";
   1.114 -
   1.115 -time_use_thy "Unification";