--- a/IntEx.thy	Tue Nov 03 16:17:19 2009 +0100
+++ b/IntEx.thy	Tue Nov 03 16:51:33 2009 +0100
@@ -14,13 +14,15 @@
 
 print_theorems
 
-quotient_def (for my_int)
+quotient_def 
   ZERO::"my_int"
 where
   "ZERO \<equiv> (0::nat, 0::nat)"
 
+term ZERO
+thm ZERO_def
 
-quotient_def (for my_int)
+quotient_def 
   ONE::"my_int"
 where
   "ONE \<equiv> (1::nat, 0::nat)"
@@ -33,7 +35,7 @@
 where
   "my_plus (x, y) (u, v) = (x + u, y + v)"
 
-quotient_def (for my_int)
+quotient_def 
   PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"
 where
   "PLUS \<equiv> my_plus"
@@ -48,13 +50,12 @@
 thm MPLUS_def
 thm MPLUS_def_raw
 
-
 fun
   my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
 where
   "my_neg (x, y) = (y, x)"
 
-quotient_def (for my_int)
+quotient_def 
   NEG::"my_int \<Rightarrow> my_int"
 where
   "NEG \<equiv> my_neg"
@@ -72,7 +73,7 @@
 where
   "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
-quotient_def (for my_int)
+quotient_def 
   MULT::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"
 where
   "MULT \<equiv> my_mult"
@@ -86,7 +87,7 @@
 where
   "my_le (x, y) (u, v) = (x+v \<le> u+y)"
 
-quotient_def (for my_int)
+quotient_def 
   LE :: "my_int \<Rightarrow> my_int \<Rightarrow> bool"
 where
   "LE \<equiv> my_le"