src/HOL/Integ/IntDef.thy

--- a/src/HOL/Integ/IntDef.thy	Mon Oct 08 14:30:28 2001 +0200
+++ b/src/HOL/Integ/IntDef.thy	Mon Oct 08 15:23:20 2001 +0200
@@ -15,7 +15,7 @@
   int = "UNIV//intrel"            (Equiv.quotient_def)
 
 instance
-  int :: {ord, zero, plus, times, minus}
+  int :: {ord, zero, one, plus, times, minus}
 
 defs
   zminus_def
@@ -35,7 +35,8 @@
   
 defs (*of overloaded constants*)
   
-  Zero_int_def      "0 == int 0"
+  Zero_int_def "0 == int 0"
+  One_int_def "1 == int 1"
 
   zadd_def
    "z + w ==