--- a/IntEx.thy	Tue Nov 03 14:04:21 2009 +0100
+++ b/IntEx.thy	Tue Nov 03 14:04:45 2009 +0100
@@ -19,7 +19,6 @@
 where
   "ZERO \<equiv> (0::nat, 0::nat)"
 
-thm ZERO_def
 
 quotient_def (for my_int)
   ONE::"my_int"
@@ -42,6 +41,14 @@
 term PLUS
 thm PLUS_def
 
+definition
+  "MPLUS x y \<equiv> my_plus x y"
+
+term MPLUS
+thm MPLUS_def
+thm MPLUS_def_raw
+
+
 fun
   my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
 where