src/ZF/upair.ML
changeset 6163 be8234f37e48
parent 6153 bff90585cce5
child 8127 68c6159440f1
     1.1 --- a/src/ZF/upair.ML	Fri Jan 29 16:26:12 1999 +0100
     1.2 +++ b/src/ZF/upair.ML	Fri Jan 29 17:08:20 1999 +0100
     1.3 @@ -230,8 +230,8 @@
     1.4  by (rtac theI 1);
     1.5  by (rtac classical 1);
     1.6  by (resolve_tac prems 1);
     1.7 -be (the_0 RS subst) 1;
     1.8 -ba 1;
     1.9 +by (etac (the_0 RS subst) 1);
    1.10 +by (assume_tac 1);
    1.11  qed "theI2";
    1.12  
    1.13  (*** if -- a conditional expression for formulae ***)