changeset 6298 | a336f80158c8 |
parent 6288 | 694c9c1910e8 |
child 9180 | 3bda56c0d70d |
--- a/src/ZF/equalities.ML Wed Mar 03 10:32:35 1999 +0100 +++ b/src/ZF/equalities.ML Wed Mar 03 10:36:24 1999 +0100 @@ -560,7 +560,7 @@ qed "Pow_0"; Goal "Pow (cons(a,A)) = Pow(A) Un {cons(a,X) . X: Pow(A)}"; -br equalityI 1; +by (rtac equalityI 1); by Safe_tac; by (etac swap 1); by (res_inst_tac [("a", "x-{a}")] RepFun_eqI 1);