src/HOL/ex/ROOT.ML
changeset 36962 5fb251d1c32f
parent 36793 27da0a27b76f
child 37280 0fb011773adc
equal deleted inserted replaced
36954:ef698bd61057 36962:5fb251d1c32f
     5 
     5 
     6 no_document use_thys [
     6 no_document use_thys [
     7   "State_Monad",
     7   "State_Monad",
     8   "Efficient_Nat_examples",
     8   "Efficient_Nat_examples",
     9   "FuncSet",
     9   "FuncSet",
    10   "Word",
       
    11   "Eval_Examples",
    10   "Eval_Examples",
    12   "Codegenerator_Test",
    11   "Codegenerator_Test",
    13   "Codegenerator_Pretty_Test",
    12   "Codegenerator_Pretty_Test",
    14   "NormalForm"
    13   "NormalForm"
    15 ];
    14 ];
    44   "Groebner_Examples",
    43   "Groebner_Examples",
    45   "MT",
    44   "MT",
    46   "Unification",
    45   "Unification",
    47   "Primrec",
    46   "Primrec",
    48   "Tarski",
    47   "Tarski",
    49   "Adder",
       
    50   "Classical",
    48   "Classical",
    51   "set",
    49   "set",
    52   "Meson_Test",
    50   "Meson_Test",
    53   "Termination",
    51   "Termination",
    54   "Coherent",
    52   "Coherent",