defining 0::int to be (int 0)

--- a/src/HOL/Integ/IntDef.ML	Tue May 23 18:08:52 2000 +0200
+++ b/src/HOL/Integ/IntDef.ML	Tue May 23 18:14:57 2000 +0200
@@ -7,6 +7,9 @@
 *)
 
 
+(*Rewrite the overloaded 0::int to (int 0)*)
+Addsimps [Zero_def];
+
 (*** Proving that intrel is an equivalence relation ***)
 
 val eqa::eqb::prems = goal Arith.thy 

--- a/src/HOL/Integ/IntDef.thy	Tue May 23 18:08:52 2000 +0200
+++ b/src/HOL/Integ/IntDef.thy	Tue May 23 18:14:57 2000 +0200
@@ -15,7 +15,7 @@
   int = "UNIV/intrel"            (Equiv.quotient_def)
 
 instance
-  int :: {ord, plus, times, minus}
+  int :: {ord, zero, plus, times, minus}
 
 defs
   zminus_def
@@ -34,6 +34,8 @@
   "iszero z == z = int 0"
   
 defs
+  Zero_def      "0 == int 0"
+
   zadd_def
    "z + w == 
        Abs_Integ(UN (x1,y1):Rep_Integ(z). UN (x2,y2):Rep_Integ(w).