--- a/IntEx.thy	Mon Oct 26 14:16:32 2009 +0100
+++ b/IntEx.thy	Mon Oct 26 14:18:26 2009 +0100
@@ -23,6 +23,13 @@
 term ZERO
 thm ZERO_def
 
+(*
+quotient_def (with my_int)
+  ZERO :: "my_int"
+where
+  "ZERO \<equiv> (0::nat, 0::nat)"
+*)
+
 local_setup {*
   make_const_def @{binding ONE} @{term "(1::nat, 0::nat)"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd
 *}