--- a/doc-src/TutorialI/Rules/Blast.thy Mon May 02 22:19:28 2011 +0200
+++ b/doc-src/TutorialI/Rules/Blast.thy Mon May 02 22:31:46 2011 +0200
@@ -1,4 +1,3 @@
-(* ID: $Id$ *)
theory Blast imports Main begin
lemma "((\<exists>x. \<forall>y. p(x)=p(y)) = ((\<exists>x. q(x))=(\<forall>y. p(y)))) =