--- a/Quot/Examples/FSet3.thy	Fri Feb 12 15:50:43 2010 +0100
+++ b/Quot/Examples/FSet3.thy	Fri Feb 12 16:04:10 2010 +0100
@@ -136,7 +136,7 @@
 
 quotient_definition
   "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "|\<union>|" 65)
-as
+is
   "op @"
 
 section {* Cardinality of finite sets *}
@@ -227,12 +227,12 @@
 
 quotient_definition
   "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
-as
+is
  "map"
 
 quotient_definition
   "fconcat :: ('a fset) fset => 'a fset"
-as
+is
  "concat"
 
 (*lemma fconcat_rsp[quot_respect]:
@@ -619,19 +619,19 @@
 
 quotient_definition
   "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" 
-  as "delete_raw"
+  is "delete_raw"
 
 quotient_definition
   "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)
-  as "inter_raw"
+  is "inter_raw"
 
 quotient_definition
   "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" 
-  as "fold_raw"
+  is "fold_raw"
 
 quotient_definition
   "fset_to_set :: 'a fset \<Rightarrow> 'a set" 
-  as "set"
+  is "set"
 
 
 section {* Lifted Theorems *}
@@ -690,7 +690,7 @@
 
 quotient_definition
   "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
-as
+is
   "list_case"
 
 (* NOT SURE IF TRUE *)