--- a/IntEx.thy	Mon Nov 02 15:39:25 2009 +0100
+++ b/IntEx.thy	Mon Nov 02 18:16:19 2009 +0100
@@ -41,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