changeset 4641 | 70a50c2a920f |
parent 4195 | 7f7bf0bd0f63 |
child 4686 | 74a12e86b20b |
--- a/src/HOL/Integ/Bin.ML Fri Feb 20 17:56:39 1998 +0100 +++ b/src/HOL/Integ/Bin.ML Fri Feb 20 17:56:51 1998 +0100 @@ -230,7 +230,6 @@ by (ALLGOALS(asm_simp_tac (simpset() addsimps[zminus_zadd_distrib RS sym, znat_add RS sym]))); - by (stac eq_False_conv 1); by (rtac notI 1); by (dres_inst_tac [("f","(% z. z + $# Suc (Suc (n + n)))")] arg_cong 1); by (Asm_full_simp_tac 1);