--- a/Quot/Examples/AbsRepTest.thy	Thu Jan 07 16:51:38 2010 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Fri Jan 08 10:08:01 2010 +0100
@@ -135,7 +135,7 @@
   apply(simp add: Quotient_abs_rep[OF a])
   done
 
-lemma set_in_eq: "(\<forall>e. ((e \<in> A) = (e \<in> B))) \<equiv> A = B"
+lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B"
   apply (rule eq_reflection)
   apply auto
   done
@@ -145,77 +145,6 @@
   apply(simp only: set_map set_in_eq)
   done
 
-lemma quotient_compose_list_pre:
- "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r s =
-       ((list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r r \<and>
-        (list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) s s \<and>
-        abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
-  apply rule
-  apply rule
-  apply rule
-  apply (rule list_rel_refl)
-  apply (metis equivp_def fset_equivp)
-  apply rule
-  apply (rule equivp_reflp[OF fset_equivp])
-  apply (rule list_rel_refl)
-  apply (metis equivp_def fset_equivp)
-  apply(rule)
-  apply rule
-  apply (rule list_rel_refl)
-  apply (metis equivp_def fset_equivp)
-  apply rule
-  apply (rule equivp_reflp[OF fset_equivp])
-  apply (rule list_rel_refl)
-  apply (metis equivp_def fset_equivp)
-  apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s")
-  apply (metis Quotient_rel[OF Quotient_fset])
-  apply (auto)[1]
-  apply (subgoal_tac "map abs_fset r = map abs_fset b")
-  prefer 2
-  apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])
-  apply (subgoal_tac "map abs_fset s = map abs_fset ba")
-  prefer 2
-  apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])
-  apply (simp add: map_rel_cong)
-  apply rule
-  apply (rule rep_abs_rsp[of "list_rel op \<approx>1" "map abs_fset"])
-  apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
-  apply (rule list_rel_refl)
-  apply (metis equivp_def fset_equivp)
-  apply rule
-  prefer 2
-  apply (rule rep_abs_rsp_left[of "list_rel op \<approx>1" "map abs_fset"])
-  apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
-  apply (rule list_rel_refl)
-  apply (metis equivp_def fset_equivp)
-  apply (erule conjE)+
-  apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s")
-  prefer 2
-  apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp)
-  apply (rule map_rel_cong)
-  apply (assumption)
-  done
-
-lemma quotient_compose_list:
-  shows  "Quotient ((list_rel op \<approx>1) OO (op \<approx>1) OO (list_rel op \<approx>1))
-  (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
-  unfolding Quotient_def comp_def
-  apply (rule)+
-  apply (simp add: abs_o_rep[OF Quotient_fset] id_simps Quotient_abs_rep[OF Quotient_fset])
-  apply (rule)
-  apply (rule)
-  apply (rule)
-  apply (rule list_rel_refl)
-  apply (metis equivp_def fset_equivp)
-  apply (rule)
-  apply (rule equivp_reflp[OF fset_equivp])
-  apply (rule list_rel_refl)
-  apply (metis equivp_def fset_equivp)
-  apply rule
-  apply rule
-apply(rule quotient_compose_list_pre)
-done
-
 lemma quotient_compose_list_gen_pre:
   assumes a: "equivp r2"
   and b: "Quotient r2 abs2 rep2"