expandshort
authorpaulson
Wed Mar 03 10:36:24 1999 +0100 (1999-03-03)
changeset 6298a336f80158c8
parent 6297 5b9fbdfe22b7
child 6299 1a88db6e7c7e
expandshort
src/ZF/equalities.ML
     1.1 --- a/src/ZF/equalities.ML	Wed Mar 03 10:32:35 1999 +0100
     1.2 +++ b/src/ZF/equalities.ML	Wed Mar 03 10:36:24 1999 +0100
     1.3 @@ -560,7 +560,7 @@
     1.4  qed "Pow_0";
     1.5  
     1.6  Goal "Pow (cons(a,A)) = Pow(A) Un {cons(a,X) . X: Pow(A)}";
     1.7 -br equalityI 1;
     1.8 +by (rtac equalityI 1);
     1.9  by Safe_tac;
    1.10  by (etac swap 1);
    1.11  by (res_inst_tac [("a", "x-{a}")] RepFun_eqI 1);