src/HOL/Library/Quotient_Set.thy
changeset 45970 b6d0cff57d96
parent 44873 045fedcfadf6
child 47094 1a7ad2601cb5
     1.1 --- a/src/HOL/Library/Quotient_Set.thy	Sat Dec 24 15:53:10 2011 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Set.thy	Sat Dec 24 15:53:10 2011 +0100
     1.3 @@ -76,20 +76,10 @@
     1.4  
     1.5  lemma mem_prs[quot_preserve]:
     1.6    assumes "Quotient R Abs Rep"
     1.7 -  shows "(Rep ---> (Abs ---> id) ---> id) (op \<in>) = op \<in>"
     1.8 -using Quotient_abs_rep[OF assms]
     1.9 -by(simp add: fun_eq_iff mem_def)
    1.10 -
    1.11 -lemma mem_rsp[quot_respect]:
    1.12 -  "(R ===> (R ===> op =) ===> op =) (op \<in>) (op \<in>)"
    1.13 -  by (auto simp add: fun_eq_iff mem_def intro!: fun_relI elim: fun_relE)
    1.14 -
    1.15 -lemma mem_prs2:
    1.16 -  assumes "Quotient R Abs Rep"
    1.17    shows "(Rep ---> op -` Abs ---> id) op \<in> = op \<in>"
    1.18    by (simp add: fun_eq_iff Quotient_abs_rep[OF assms])
    1.19  
    1.20 -lemma mem_rsp2:
    1.21 +lemma mem_rsp[quot_respect]:
    1.22    shows "(R ===> set_rel R ===> op =) op \<in> op \<in>"
    1.23    by (intro fun_relI) (simp add: set_rel_def)
    1.24