src/ZF/OrdQuant.thy

--- a/src/ZF/OrdQuant.thy	Tue May 14 12:33:42 2002 +0200
+++ b/src/ZF/OrdQuant.thy	Wed May 15 10:42:32 2002 +0200
@@ -84,7 +84,7 @@
 by (simp add: function_def lam_def) 
 
 lemma relation_lam: "relation (lam x:A. b(x))"  
-by (simp add: relation_def lam_def, blast) 
+by (simp add: relation_def lam_def) 
 
 lemma restrict_iff: "z \<in> restrict(r,A) \<longleftrightarrow> z \<in> r & (\<exists>x\<in>A. \<exists>y. z = \<langle>x, y\<rangle>)"
 by (simp add: restrict_def)