changeset 33688 | 1a97dcd8dc6a |
parent 33615 | 261abc2e3155 |
child 35247 | 0831bd85eee5 |
--- a/src/HOL/Induct/ROOT.ML Sat Nov 14 18:45:24 2009 +0100 +++ b/src/HOL/Induct/ROOT.ML Sat Nov 14 19:56:18 2009 +0100 @@ -2,5 +2,4 @@ use_thys ["Common_Patterns"]; use_thys ["QuoDataType", "QuoNestedDataType", "Term", - "ABexp", "Tree", "Ordinals", "Sigma_Algebra", "Comb", "PropLog", - "SList", "LFilter", "Com"]; + "ABexp", "Tree", "Ordinals", "Sigma_Algebra", "Comb", "PropLog", "Com"];