src/Pure/Isar/skip_proof.ML
changeset 17476 315cb57e3dd7
parent 17362 c089fa02c1e5
child 17956 369e2af8ee45
     1.1 --- a/src/Pure/Isar/skip_proof.ML	Sat Sep 17 19:17:34 2005 +0200
     1.2 +++ b/src/Pure/Isar/skip_proof.ML	Sat Sep 17 19:17:35 2005 +0200
     1.3 @@ -5,9 +5,6 @@
     1.4  Skipping proofs -- quick_and_dirty mode.
     1.5  *)
     1.6  
     1.7 -(*if true then some tools will OMIT some proofs*)
     1.8 -val quick_and_dirty = ref false;
     1.9 -
    1.10  signature SKIP_PROOF =
    1.11  sig
    1.12    val make_thm: theory -> term -> thm