src/HOL/Integ/IntDef.ML
changeset 8949 d46adac29b71
parent 8937 7328d7c8d201
child 9108 9fff97d29837
     1.1 --- a/src/HOL/Integ/IntDef.ML	Wed May 24 18:40:01 2000 +0200
     1.2 +++ b/src/HOL/Integ/IntDef.ML	Wed May 24 18:41:09 2000 +0200
     1.3 @@ -228,6 +228,11 @@
     1.4  Addsimps [zadd_int0, zadd_int0_right,
     1.5  	  zadd_zminus_inverse, zadd_zminus_inverse2];
     1.6  
     1.7 +(*for the instance declaration int :: plus_ac0*)
     1.8 +Goal "0 + z = (z::int)";
     1.9 +by (Simp_tac 1);
    1.10 +qed "zadd_zero";
    1.11 +
    1.12  Goal "z + (- z + w) = (w::int)";
    1.13  by (simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
    1.14  qed "zadd_zminus_cancel";