author | wenzelm |
Sat, 27 Sep 2008 19:35:00 +0200 | |
changeset 28385 | 74c6d73a8b2e |
parent 28384 | 70abca69247b |
child 28386 | f2f1dd50da5a |
--- a/src/HOL/Induct/ROOT.ML Sat Sep 27 18:18:08 2008 +0200 +++ b/src/HOL/Induct/ROOT.ML Sat Sep 27 19:35:00 2008 +0200 @@ -1,7 +1,7 @@ (* $Id$ *) -setmp quick_and_dirty true +setmp_noncritical quick_and_dirty true use_thy "Common_Patterns"; use_thys ["Mutil", "QuoDataType", "QuoNestedDataType", "Term",