diff -r 93c9022ba5e9 -r c4001cda9da3 Quot/Examples/SigmaEx.thy
--- a/Quot/Examples/SigmaEx.thy	Fri Feb 12 15:50:43 2010 +0100
+++ b/Quot/Examples/SigmaEx.thy	Fri Feb 12 16:04:10 2010 +0100
@@ -35,27 +35,27 @@
 
 quotient_definition
   "Var :: name \<Rightarrow> obj"
-as
+is
   "rVar"
 
 quotient_definition
   "Obj :: (string \<times> method) list \<Rightarrow> obj"
-as
+is
   "rObj"
 
 quotient_definition
   "Inv :: obj \<Rightarrow> string \<Rightarrow> obj"
-as
+is
   "rInv"
 
 quotient_definition
   "Upd :: obj \<Rightarrow> string \<Rightarrow> method \<Rightarrow> obj"
-as
+is
   "rUpd"
 
 quotient_definition
   "Sig :: name \<Rightarrow> obj \<Rightarrow> method"
-as
+is
   "rSig"
 
 overloading
@@ -65,12 +65,12 @@
 
 quotient_definition
   "perm_obj :: 'x prm \<Rightarrow> obj \<Rightarrow> obj"
-as
+is
   "(perm::'x prm \<Rightarrow> robj \<Rightarrow> robj)"
 
 quotient_definition
   "perm_method :: 'x prm \<Rightarrow> method \<Rightarrow> method"
-as
+is
   "(perm::'x prm \<Rightarrow> rmethod \<Rightarrow> rmethod)"
 
 end