changeset 67399 | eab6ce8368fa |
parent 66364 | fa3247e6ee4b |
child 71393 | fce780f9c9c6 |
--- a/src/HOL/Equiv_Relations.thy Wed Jan 10 15:21:49 2018 +0100 +++ b/src/HOL/Equiv_Relations.thy Wed Jan 10 15:25:09 2018 +0100 @@ -472,7 +472,7 @@ lemma equivp_reflp_symp_transp: "equivp R \<longleftrightarrow> reflp R \<and> symp R \<and> transp R" by (auto intro: equivpI elim: equivpE) -lemma identity_equivp: "equivp (op =)" +lemma identity_equivp: "equivp (=)" by (auto intro: equivpI reflpI sympI transpI) lemma equivp_reflp: "equivp R \<Longrightarrow> R x x"