diff -r 2b3c7e319d82 -r 895994073bdf src/ZF/QPair.thy
--- a/src/ZF/QPair.thy Wed Aug 28 13:08:34 2002 +0200
+++ b/src/ZF/QPair.thy Wed Aug 28 13:08:50 2002 +0200
@@ -126,10 +126,10 @@
subsubsection{*Projections: qfst, qsnd*}
lemma qfst_conv [simp]: "qfst() = a"
-by (simp add: qfst_def, blast)
+by (simp add: qfst_def)
lemma qsnd_conv [simp]: "qsnd() = b"
-by (simp add: qsnd_def, blast)
+by (simp add: qsnd_def)
lemma qfst_type [TC]: "p:QSigma(A,B) ==> qfst(p) : A"
by auto