src/ZF/pair.thy
changeset 17001 51ff2bc32774
parent 16417 9bc16273c2d4
child 24893 b8ef7afe3a6b
     1.1 --- a/src/ZF/pair.thy	Tue Aug 02 16:52:21 2005 +0200
     1.2 +++ b/src/ZF/pair.thy	Tue Aug 02 19:47:11 2005 +0200
     1.3 @@ -129,7 +129,8 @@
     1.4  lemma expand_split: 
     1.5    "u: A*B ==>    
     1.6          R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))"
     1.7 -apply (simp add: split_def, auto)
     1.8 +apply (simp add: split_def)
     1.9 +apply auto
    1.10  done
    1.11  
    1.12