src/HOL/Induct/ROOT.ML
changeset 33615 261abc2e3155
parent 28827 b3ce1912ac25
child 33688 1a97dcd8dc6a
equal deleted inserted replaced
33608:5c0024338cef 33615:261abc2e3155
     1 
       
     2 (* $Id$ *)
       
     3 
       
     4 setmp_noncritical quick_and_dirty true
     1 setmp_noncritical quick_and_dirty true
     5   use_thy "Common_Patterns";
     2   use_thys ["Common_Patterns"];
     6 
     3 
     7 use_thys ["QuoDataType", "QuoNestedDataType", "Term",
     4 use_thys ["QuoDataType", "QuoNestedDataType", "Term",
     8   "ABexp", "Tree", "Ordinals", "Sigma_Algebra", "Comb", "PropLog",
     5   "ABexp", "Tree", "Ordinals", "Sigma_Algebra", "Comb", "PropLog",
     9   "SList", "LFilter", "Com"];
     6   "SList", "LFilter", "Com"];