| changeset 11464 | ddea204de5bc |
| parent 11018 | 71d624788ce2 |
| child 11701 | 3d51fbf81c17 |
--- a/src/HOL/Integ/nat_bin.ML Mon Aug 06 13:12:06 2001 +0200 +++ b/src/HOL/Integ/nat_bin.ML Mon Aug 06 13:43:24 2001 +0200 @@ -495,7 +495,7 @@ by Auto_tac; val lemma1 = result(); -Goal "m+m ~= int 1 + n + n"; +Goal "m+m ~= int 1' + n + n"; by Auto_tac; by (dres_inst_tac [("f", "%x. x mod #2")] arg_cong 1); by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1);