diff -r 24799397a3ce -r 7fbbb2690bc5 FSet.thy
--- a/FSet.thy	Wed Dec 02 10:56:35 2009 +0100
+++ b/FSet.thy	Wed Dec 02 11:30:40 2009 +0100
@@ -371,7 +371,6 @@
 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-
 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* C *) (* = and extensionality *)
 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *)
 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
@@ -380,22 +379,22 @@
 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
 apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 7 *) (* respectfulness *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 7 *) (* respectfulness *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 done
 
 quotient_def