--- a/IntEx.thy	Wed Nov 04 09:52:31 2009 +0100
+++ b/IntEx.thy	Wed Nov 04 10:31:20 2009 +0100
@@ -13,6 +13,7 @@
   done
 
 print_theorems
+print_quotients
 
 quotient_def 
   ZERO::"my_int"
@@ -38,18 +39,11 @@
 quotient_def 
   PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"
 where
-  "PLUS \<equiv> my_plus"
+  "PLUS x y \<equiv> my_plus x y"
 
 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