src/ZF/pair.thy

--- a/src/ZF/pair.thy	Tue Aug 02 16:52:21 2005 +0200
+++ b/src/ZF/pair.thy	Tue Aug 02 19:47:11 2005 +0200
@@ -129,7 +129,8 @@
 lemma expand_split: 
   "u: A*B ==>    
         R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))"
-apply (simp add: split_def, auto)
+apply (simp add: split_def)
+apply auto
 done