--- a/FSet.thy	Sat Nov 28 18:49:39 2009 +0100
+++ b/FSet.thy	Sat Nov 28 19:14:12 2009 +0100
@@ -398,7 +398,6 @@
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 done
 
-
 quotient_def
   fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 where