| changeset 10566 | 7ed4f5a6c63f |
| parent 10259 | 93ec82d535f2 |
| child 10876 | e12892e4666a |
--- a/src/HOL/Induct/ROOT.ML Fri Dec 01 19:41:09 2000 +0100 +++ b/src/HOL/Induct/ROOT.ML Fri Dec 01 19:41:45 2000 +0100 @@ -8,7 +8,6 @@ time_use_thy "Mutil"; time_use_thy "PropLog"; time_use_thy "SList"; -setmp quick_and_dirty false (* FIXME tmp hack *) time_use_thy "LFilter"; time_use_thy "Term"; time_use_thy "ABexp";