# HG changeset patch
# User wenzelm
# Date 1126977455 -7200
# Node ID 315cb57e3dd73d210dad64f1618762d93a94d5d9
# Parent  d008d04068a16a0e58403b9c774cfe0945181442
moved quick_and_dirty to Pure/ROOT.ML;

diff -r d008d04068a1 -r 315cb57e3dd7 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