# HG changeset patch
# User paulson
# Date 959098497 -7200
# Node ID 7328d7c8d20181bc54112b2bcaa47eff00d22b82
# Parent  a1c42654175776f8f33048d5784fc9c7ff548191
defining 0::int to be (int 0)

diff -r a1c426541757 -r 7328d7c8d201 src/HOL/Integ/IntDef.ML
--- 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 
diff -r a1c426541757 -r 7328d7c8d201 src/HOL/Integ/IntDef.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).