src/ZF/OrdQuant.thy
changeset 13149 773657d466cb
parent 13118 336b0bcbd27c
child 13162 660a71e712af
     1.1 --- a/src/ZF/OrdQuant.thy	Tue May 14 12:33:42 2002 +0200
     1.2 +++ b/src/ZF/OrdQuant.thy	Wed May 15 10:42:32 2002 +0200
     1.3 @@ -84,7 +84,7 @@
     1.4  by (simp add: function_def lam_def) 
     1.5  
     1.6  lemma relation_lam: "relation (lam x:A. b(x))"  
     1.7 -by (simp add: relation_def lam_def, blast) 
     1.8 +by (simp add: relation_def lam_def) 
     1.9  
    1.10  lemma restrict_iff: "z \<in> restrict(r,A) \<longleftrightarrow> z \<in> r & (\<exists>x\<in>A. \<exists>y. z = \<langle>x, y\<rangle>)"
    1.11  by (simp add: restrict_def)