run Mirabelle in quick and dirty mode
authorblanchet
Tue, 24 Apr 2012 09:47:40 +0200
changeset 47712 81c3c4e01263
parent 47711 c1cca2a052e4
child 47713 bd0683000a0f
run Mirabelle in quick and dirty mode
src/HOL/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Tue Apr 24 09:09:55 2012 +0200
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Tue Apr 24 09:47:40 2012 +0200
@@ -138,7 +138,7 @@
 if ($output_log) { print "Mirabelle: $thy_file\n"; }
 
 my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
-  "-e 'use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet;
+  "-e 'Unsynchronized.setmp quick_and_dirty true use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet;
 
 if ($output_log) { print "Finished:  $thy_file\n"; }