diff -r 84a38acbf512 -r 538daee762e6 Quot/Examples/FSet2.thy
--- a/Quot/Examples/FSet2.thy	Mon Feb 15 10:25:17 2010 +0100
+++ b/Quot/Examples/FSet2.thy	Mon Feb 15 12:15:14 2010 +0100
@@ -21,12 +21,14 @@
 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
 by (auto intro: list_eq.intros list_eq_refl)
 
-quotient_type 
+quotient_type
   'a fset = "'a list" / "list_eq"
   by (rule equivp_list_eq)
 
 quotient_definition
-  "fempty :: 'a fset" ("{||}")
+  fempty ("{||}")
+where
+  "fempty :: 'a fset"
 is
   "[]"
 
@@ -40,7 +42,9 @@
 by (auto intro: list_eq.intros)
 
 quotient_definition
-  "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [65,66] 65)
+  funion ("_ \<union>f _" [65,66] 65)
+where
+  "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 is
   "(op @)"
 
@@ -67,7 +71,9 @@
 
 
 quotient_definition
-  "fmem :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50)
+  fmem ("_ \<in>f _" [50, 51] 50)
+where
+  "fmem :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"
 is
   "(op mem)"
 
@@ -80,7 +86,7 @@
   shows "(op = ===> (op \<approx> ===> op =)) (op mem) (op mem)"
   by (simp add: memb_rsp_aux)
 
-definition 
+definition
   fnot_mem :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<notin>f _" [50, 51] 50)
 where
   "x \<notin>f S \<equiv> \<not>(x \<in>f S)"
@@ -91,7 +97,9 @@
   "inter_list X Y \<equiv> [x \<leftarrow> X. x\<in>set Y]"
 
 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_list"