src/HOL/Equiv_Relations.thy
changeset 63092 a949b2a5f51d
parent 61952 546958347e05
child 63653 4453cfb745e5
     1.1 --- a/src/HOL/Equiv_Relations.thy	Fri May 13 20:22:02 2016 +0200
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Fri May 13 20:24:10 2016 +0200
     1.3 @@ -266,7 +266,7 @@
     1.4  
     1.5  lemma congruent2D:
     1.6    "congruent2 r1 r2 f \<Longrightarrow> (y1, z1) \<in> r1 \<Longrightarrow> (y2, z2) \<in> r2 \<Longrightarrow> f y1 y2 = f z1 z2"
     1.7 -  using assms by (auto simp add: congruent2_def)
     1.8 +  by (auto simp add: congruent2_def)
     1.9  
    1.10  text\<open>Abbreviation for the common case where the relations are identical\<close>
    1.11  abbreviation
    1.12 @@ -426,7 +426,7 @@
    1.13  
    1.14  lemma in_quotient_imp_subset:
    1.15  "\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> X \<subseteq> A"
    1.16 -using assms in_quotient_imp_in_rel equiv_type by fastforce
    1.17 +using in_quotient_imp_in_rel equiv_type by fastforce
    1.18  
    1.19  
    1.20  subsection \<open>Equivalence relations -- predicate version\<close>