--- a/Quot/Examples/FSet3.thy	Mon Feb 15 10:25:17 2010 +0100
+++ b/Quot/Examples/FSet3.thy	Mon Feb 15 12:15:14 2010 +0100
@@ -32,7 +32,9 @@
 section {* empty fset, finsert and membership *} 
 
 quotient_definition
-  "fempty :: 'a fset" ("{||}")
+  fempty  ("{||}")
+where
+  "fempty :: 'a fset"
 is "[]::'a list"
 
 quotient_definition
@@ -52,7 +54,9 @@
   "memb x xs \<equiv> x \<in> set xs"
 
 quotient_definition
-  "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<in>| _" [50, 51] 50)
+  fin ("_ |\<in>| _" [50, 51] 50)
+where
+  "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"
 is "memb"
 
 abbreviation
@@ -135,7 +139,9 @@
 section {* Union *}
 
 quotient_definition
-  "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "|\<union>|" 65)
+  funion  (infixl "|\<union>|" 65)
+where
+  "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 is
   "op @"
 
@@ -622,7 +628,9 @@
   is "delete_raw"
 
 quotient_definition
-  "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)
+  finter ("_ \<inter>f _" [70, 71] 70)
+where
+  "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
   is "inter_raw"
 
 quotient_definition
@@ -703,7 +711,4 @@
 apply (lifting list.cases(2))
 done
 
-thm quot_respect
-
-
 end