--- a/src/HOL/Int.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Int.thy Wed Nov 30 16:27:10 2011 +0100
@@ -18,9 +18,11 @@
definition intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set" where
"intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
-typedef (Integ)
- int = "UNIV//intrel"
- by (auto simp add: quotient_def)
+definition "Integ = UNIV//intrel"
+
+typedef (open) int = Integ
+ morphisms Rep_Integ Abs_Integ
+ unfolding Integ_def by (auto simp add: quotient_def)
instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
begin