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