# HG changeset patch # User wenzelm # Date 975696105 -3600 # Node ID 7ed4f5a6c63f28a0c23147dd7f8b4a3ee6dbc6ca # Parent 7f7c1c3511e2a858f09af117471feb46515b6afb removed quick_and_dirty; diff -r 7f7c1c3511e2 -r 7ed4f5a6c63f src/HOL/Induct/ROOT.ML --- 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";