changeset 12667 | 7e6eaaa125f2 |
parent 11317 | 7f9e4c389318 |
--- a/src/ZF/AC/AC7_AC9.ML Tue Jan 08 15:39:47 2002 +0100 +++ b/src/ZF/AC/AC7_AC9.ML Tue Jan 08 16:09:09 2002 +0100 @@ -161,7 +161,8 @@ \ B1: C; B2: C |] \ \ ==> B1 eqpoll B2"; by (blast_tac - (claset() addSIs [nat_lepoll_lemma, nat_cons_eqpoll RS eqpoll_trans, + (claset() delrules [eqpoll_refl] + addSIs [nat_lepoll_lemma, nat_cons_eqpoll RS eqpoll_trans, eqpoll_refl RSN (2, prod_eqpoll_cong)] addIs [eqpoll_trans, eqpoll_sym, Sigma_fun_space_eqpoll]) 1); val lemma1 = result();