# HG changeset patch
# User paulson
# Date 959186469 -7200
# Node ID d46adac29b713ee040a4a42c39545761c703abf0
# Parent  b797cfa3548d8cf05704107f696511201ab87b5d
installing plus_ac0 for int

diff -r b797cfa3548d -r d46adac29b71 src/HOL/Integ/Int.thy
--- 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
diff -r b797cfa3548d -r d46adac29b71 src/HOL/Integ/IntDef.ML
--- 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";