--- a/src/HOL/Integ/Int.thy Wed May 24 18:40:01 2000 +0200
+++ b/src/HOL/Integ/Int.thy Wed May 24 18:41:09 2000 +0200
@@ -9,6 +9,7 @@
Int = IntDef +
instance int :: order (zle_refl,zle_trans,zle_anti_sym,int_less_le)
+instance int :: plus_ac0 (zadd_commute,zadd_assoc,zadd_zero)
instance int :: linorder (zle_linear)
constdefs
--- 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";