--- a/Quot/Examples/IntEx.thy	Sun Dec 20 00:26:53 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Sun Dec 20 00:53:35 2009 +0100
@@ -21,12 +21,12 @@
 print_theorems
 print_quotients
 
-quotient_def
+quotient_definition
   "ZERO :: my_int"
 as
   "(0::nat, 0::nat)"
 
-quotient_def
+quotient_definition
   "ONE :: my_int"
 as
   "(1::nat, 0::nat)"
@@ -36,7 +36,7 @@
 where
   "my_plus (x, y) (u, v) = (x + u, y + v)"
 
-quotient_def
+quotient_definition
   "PLUS :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
 as
   "my_plus"
@@ -46,7 +46,7 @@
 where
   "my_neg (x, y) = (y, x)"
 
-quotient_def
+quotient_definition
   "NEG :: my_int \<Rightarrow> my_int"
 as
   "my_neg"
@@ -61,7 +61,7 @@
 where
   "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
-quotient_def
+quotient_definition
   "MULT :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
 as
   "my_mult"
@@ -73,7 +73,7 @@
 where
   "my_le (x, y) (u, v) = (x+v \<le> u+y)"
 
-quotient_def
+quotient_definition
    "LE :: my_int \<Rightarrow> my_int \<Rightarrow> bool"
 as
   "my_le"