--- a/src/HOL/Integ/IntDef.thy Wed Jul 19 12:33:19 2000 +0200
+++ b/src/HOL/Integ/IntDef.thy Wed Jul 19 12:33:36 2000 +0200
@@ -9,10 +9,10 @@
IntDef = Equiv + Arith +
constdefs
intrel :: "((nat * nat) * (nat * nat)) set"
- "intrel == {p. ? x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}"
+ "intrel == {p. EX x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}"
typedef (Integ)
- int = "UNIV/intrel" (Equiv.quotient_def)
+ int = "UNIV//intrel" (Equiv.quotient_def)
instance
int :: {ord, zero, plus, times, minus}
@@ -33,7 +33,8 @@
iszero :: int => bool
"iszero z == z = int 0"
-defs
+defs (*of overloaded constants*)
+
Zero_def "0 == int 0"
zadd_def