turn on quick and dirty in batch mode
authorhaftmann
Sat, 03 Mar 2012 22:38:11 +0100
changeset 46789 074dc33767a5
parent 46788 aefdc0095d7e
child 46790 f3c10e908f65
turn on quick and dirty in batch mode
src/HOL/Import/HOL4/imported.ML
src/HOL/Import/HOL_Light/imported.ML
--- a/src/HOL/Import/HOL4/imported.ML	Sat Mar 03 22:37:56 2012 +0100
+++ b/src/HOL/Import/HOL4/imported.ML	Sat Mar 03 22:38:11 2012 +0100
@@ -1,2 +1,2 @@
 
-use_thy "Imported";
+Unsynchronized.setmp quick_and_dirty true use_thy "Imported";
--- a/src/HOL/Import/HOL_Light/imported.ML	Sat Mar 03 22:37:56 2012 +0100
+++ b/src/HOL/Import/HOL_Light/imported.ML	Sat Mar 03 22:38:11 2012 +0100
@@ -1,2 +1,2 @@
 
-use_thy "Imported";
+Unsynchronized.setmp quick_and_dirty true use_thy "Imported";