diff -r df053507edba -r 37285ec4387d Quot/Examples/LarryInt.thy
--- a/Quot/Examples/LarryInt.thy	Sun Dec 20 00:26:53 2009 +0100
+++ b/Quot/Examples/LarryInt.thy	Sun Dec 20 00:53:35 2009 +0100
@@ -16,16 +16,16 @@
 instantiation int :: "{zero, one, plus, uminus, minus, times, ord}"
 begin
 
-quotient_def 
+quotient_definition 
   Zero_int_def: "0::int" as "(0::nat, 0::nat)"
 
-quotient_def
+quotient_definition
   One_int_def: "1::int" as "(1::nat, 0::nat)"
 
 definition
   "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u::nat), y + (v::nat))"
 
-quotient_def
+quotient_definition
   "(op +) :: int \<Rightarrow> int \<Rightarrow> int" 
 as 
   "add_raw"
@@ -33,7 +33,7 @@
 definition
   "uminus_raw \<equiv> \<lambda>(x::nat, y::nat). (y, x)"
 
-quotient_def
+quotient_definition
   "uminus :: int \<Rightarrow> int" 
 as 
   "uminus_raw"
@@ -43,7 +43,7 @@
 where
   "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
-quotient_def
+quotient_definition
   "(op *) :: int \<Rightarrow> int \<Rightarrow> int" 
 as 
   "mult_raw"
@@ -51,7 +51,7 @@
 definition
   "le_raw \<equiv> \<lambda>(x, y) (u, v). (x+v \<le> u+(y::nat))"
 
-quotient_def 
+quotient_definition 
   le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" 
 as 
   "le_raw"
@@ -343,7 +343,7 @@
 definition
   "nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"
 
-quotient_def
+quotient_definition
   "nat2::int\<Rightarrow>nat"
 as
   "nat_raw"