diff -r df053507edba -r 37285ec4387d Quot/Examples/IntEx2.thy
--- a/Quot/Examples/IntEx2.thy	Sun Dec 20 00:26:53 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Sun Dec 20 00:53:35 2009 +0100
@@ -20,10 +20,10 @@
 
 ML {* @{term "0 \<Colon> int"} *}
 
-quotient_def
+quotient_definition
   "0 \<Colon> int" as "(0\<Colon>nat, 0\<Colon>nat)"
 
-quotient_def
+quotient_definition
   "1 \<Colon> int" as "(1\<Colon>nat, 0\<Colon>nat)"
 
 fun
@@ -31,7 +31,7 @@
 where
   "plus_raw (x, y) (u, v) = (x + u, y + v)"
 
-quotient_def
+quotient_definition
   "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" as "plus_raw"
 
 fun
@@ -39,7 +39,7 @@
 where
   "uminus_raw (x, y) = (y, x)"
 
-quotient_def
+quotient_definition
   "(uminus \<Colon> (int \<Rightarrow> int))" as "uminus_raw"
 
 definition
@@ -50,7 +50,7 @@
 where
   "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
-quotient_def
+quotient_definition
   mult_int_def: "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" as "mult_raw"
 
 fun
@@ -58,7 +58,7 @@
 where
   "le_raw (x, y) (u, v) = (x+v \<le> u+y)"
 
-quotient_def
+quotient_definition
   le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" as "le_raw"
 
 definition
@@ -206,7 +206,7 @@
 definition int_of_nat_raw: 
   "int_of_nat_raw m = (m :: nat, 0 :: nat)"
 
-quotient_def
+quotient_definition
   "int_of_nat :: nat \<Rightarrow> int" as "int_of_nat_raw"
 
 lemma[quot_respect]: