diff -r 93c9022ba5e9 -r c4001cda9da3 Quot/Examples/LarryInt.thy
--- a/Quot/Examples/LarryInt.thy	Fri Feb 12 15:50:43 2010 +0100
+++ b/Quot/Examples/LarryInt.thy	Fri Feb 12 16:04:10 2010 +0100
@@ -16,18 +16,18 @@
 instantiation int :: "{zero, one, plus, uminus, minus, times, ord}"
 begin
 
-quotient_definition 
-  Zero_int_def: "0::int" as "(0::nat, 0::nat)"
+quotient_definition
+  Zero_int_def: "0::int" is "(0::nat, 0::nat)"
 
 quotient_definition
-  One_int_def: "1::int" as "(1::nat, 0::nat)"
+  One_int_def: "1::int" is "(1::nat, 0::nat)"
 
 definition
   "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u::nat), y + (v::nat))"
 
 quotient_definition
   "(op +) :: int \<Rightarrow> int \<Rightarrow> int" 
-as 
+is
   "add_raw"
 
 definition
@@ -35,7 +35,7 @@
 
 quotient_definition
   "uminus :: int \<Rightarrow> int" 
-as 
+is
   "uminus_raw"
 
 fun
@@ -45,7 +45,7 @@
 
 quotient_definition
   "(op *) :: int \<Rightarrow> int \<Rightarrow> int" 
-as 
+is
   "mult_raw"
 
 definition
@@ -53,7 +53,7 @@
 
 quotient_definition 
   le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" 
-as 
+is
   "le_raw"
 
 definition
@@ -369,7 +369,7 @@
 
 quotient_definition
   "nat2::int \<Rightarrow> nat"
-as
+is
   "nat_raw"
 
 abbreviation