| changeset 36096 | abc6a2ea4b88 |
| parent 35247 | 0831bd85eee5 |
| child 39616 | 8052101883c3 |
--- a/src/HOL/Induct/ROOT.ML Fri Apr 02 13:33:48 2010 +0200 +++ b/src/HOL/Induct/ROOT.ML Wed Apr 07 19:17:10 2010 +0200 @@ -1,5 +1,5 @@ setmp_noncritical quick_and_dirty true use_thys ["Common_Patterns"]; -use_thys ["QuoDataType", "QuoNestedDataType", "Term", +use_thys ["QuoDataType", "QuoNestedDataType", "Term", "SList", "ABexp", "Tree", "Ordinals", "Sigma_Algebra", "Comb", "PropLog", "Com"];