diff -r aaeb5a34d21a -r 3c8ad149a4d3 Quot/Examples/FSet3.thy
--- a/Quot/Examples/FSet3.thy	Fri Feb 12 16:06:09 2010 +0100
+++ b/Quot/Examples/FSet3.thy	Fri Feb 12 16:27:25 2010 +0100
@@ -33,11 +33,11 @@
 
 quotient_definition
   "fempty :: 'a fset" ("{||}")
-as "[]::'a list"
+is "[]::'a list"
 
 quotient_definition
   "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" 
-as "op #"
+is "op #"
 
 syntax
   "@Finset"     :: "args => 'a fset"  ("{|(_)|}")
@@ -53,7 +53,7 @@
 
 quotient_definition
   "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<in>| _" [50, 51] 50)
-as "memb"
+is "memb"
 
 abbreviation
   fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50)
@@ -149,7 +149,7 @@
 
 quotient_definition
   "fcard :: 'a fset \<Rightarrow> nat" 
-as "fcard_raw"
+is "fcard_raw"
 
 text {* raw section *}