--- a/FSet.thy	Fri Nov 27 10:04:49 2009 +0100
+++ b/FSet.thy	Fri Nov 27 13:59:52 2009 +0100
@@ -347,10 +347,14 @@
 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *})
 prefer 2
-apply (tactic {* clean_tac @{context} [quot] defs [(@{typ "('a list \<Rightarrow> bool)"},@{typ "('a fset \<Rightarrow> bool)"})] 1 *})
+apply (tactic {* clean_tac @{context} [quot] defs 
+                 [(@{typ "('a list \<Rightarrow> bool)"},@{typ "('a fset \<Rightarrow> bool)"})] 1 *})
 apply(tactic {* r_mk_comb_tac' @{context} rty [quot] rel_refl trans2 rsp_thms 1*})
 done
 
+
+
+
 quotient_def
   fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 where