moved quick_and_dirty to Pure/ROOT.ML;
authorwenzelm
Sat, 17 Sep 2005 19:17:35 +0200
changeset 17476 315cb57e3dd7
parent 17475 d008d04068a1
child 17477 ceb42ea2f223
moved quick_and_dirty to Pure/ROOT.ML;
src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Sat Sep 17 19:17:34 2005 +0200
+++ b/src/Pure/Isar/skip_proof.ML	Sat Sep 17 19:17:35 2005 +0200
@@ -5,9 +5,6 @@
 Skipping proofs -- quick_and_dirty mode.
 *)
 
-(*if true then some tools will OMIT some proofs*)
-val quick_and_dirty = ref false;
-
 signature SKIP_PROOF =
 sig
   val make_thm: theory -> term -> thm