--- a/Quot/Examples/IntEx.thy	Mon Dec 07 21:54:14 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Mon Dec 07 23:45:51 2009 +0100
@@ -153,8 +153,6 @@
 apply(rule refl)
 done
 
-
-
 lemma "PLUS a = PLUS a"
 apply(tactic {* procedure_tac @{context} @{thm test2} 1 *})
 apply(rule impI)