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