diff -r 93c9022ba5e9 -r c4001cda9da3 Quot/Examples/FSet2.thy
--- a/Quot/Examples/FSet2.thy	Fri Feb 12 15:50:43 2010 +0100
+++ b/Quot/Examples/FSet2.thy	Fri Feb 12 16:04:10 2010 +0100
@@ -27,12 +27,12 @@
 
 quotient_definition
   "fempty :: 'a fset" ("{||}")
-as
+is
   "[]"
 
 quotient_definition
   "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-as
+is
   "(op #)"
 
 lemma finsert_rsp[quot_respect]:
@@ -41,7 +41,7 @@
 
 quotient_definition
   "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [65,66] 65)
-as
+is
   "(op @)"
 
 lemma append_rsp_aux1:
@@ -68,7 +68,7 @@
 
 quotient_definition
   "fmem :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50)
-as
+is
   "(op mem)"
 
 lemma memb_rsp_aux:
@@ -92,7 +92,7 @@
 
 quotient_definition
   "finter::'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)
-as
+is
   "inter_list"
 
 no_syntax