src/HOL/ex/ROOT.ML
changeset 25543 6b2031004d3f
parent 25374 7657a081fcb4
child 25568 7bb10db582cf
equal deleted inserted replaced
25542:ced4104f6c1f 25543:6b2031004d3f
     5 *)
     5 *)
     6 
     6 
     7 no_document use_thys [
     7 no_document use_thys [
     8   "Parity",
     8   "Parity",
     9   "GCD",
     9   "GCD",
    10   "Classpackage",
       
    11   "Eval",
    10   "Eval",
    12   "State_Monad",
    11   "State_Monad",
    13   "Code_Integer",
    12   "Code_Integer",
    14   "Efficient_Nat",
    13   "Efficient_Nat",
    15   "Codegenerator",
    14   "Codegenerator",