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