--- a/Quot/Examples/LamEx.thy	Fri Feb 12 15:50:43 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Fri Feb 12 16:04:10 2010 +0100
@@ -178,22 +178,22 @@
 
 quotient_definition
   "Var :: name \<Rightarrow> lam"
-as
+is
   "rVar"
 
 quotient_definition
    "App :: lam \<Rightarrow> lam \<Rightarrow> lam"
-as
+is
   "rApp"
 
 quotient_definition
   "Lam :: name \<Rightarrow> lam \<Rightarrow> lam"
-as
+is
   "rLam"
 
 quotient_definition
   "fv :: lam \<Rightarrow> name set"
-as
+is
   "rfv"
 
 (* definition of overloaded permutation function *)
@@ -204,7 +204,7 @@
 
 quotient_definition
   "perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"
-as
+is
   "perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam"
 
 end