src/HOL/Induct/ROOT.ML
changeset 35247 0831bd85eee5
parent 33688 1a97dcd8dc6a
child 39616 8052101883c3
equal deleted inserted replaced
35246:bcbb5ba7dbbc 35247:0831bd85eee5
     1 setmp_noncritical quick_and_dirty true
     1 setmp_noncritical quick_and_dirty true
     2   use_thys ["Common_Patterns"];
     2   use_thys ["Common_Patterns"];
     3 
     3 
     4 use_thys ["QuoDataType", "QuoNestedDataType", "Term",
     4 use_thys ["QuoDataType", "QuoNestedDataType", "Term", "SList",
     5   "ABexp", "Tree", "Ordinals", "Sigma_Algebra", "Comb", "PropLog", "Com"];
     5   "ABexp", "Tree", "Ordinals", "Sigma_Algebra", "Comb", "PropLog", "Com"];