src/HOL/Equiv_Relations.thy
changeset 60688 01488b559910
parent 60517 f16e4fb20652
child 60758 d8d85a8172b5
     1.1 --- a/src/HOL/Equiv_Relations.thy	Wed Jul 08 14:01:40 2015 +0200
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Wed Jul 08 14:01:41 2015 +0200
     1.3 @@ -523,20 +523,6 @@
     1.4    "equivp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
     1.5    by (erule equivpE, erule transpE)
     1.6  
     1.7 -
     1.8 -subsection \<open>Prominent examples\<close>
     1.9 -
    1.10 -lemma equivp_associated:
    1.11 -  "equivp associated"
    1.12 -proof (rule equivpI)
    1.13 -  show "reflp associated"
    1.14 -    by (rule reflpI) simp
    1.15 -  show "symp associated"
    1.16 -    by (rule sympI) (simp add: associated_sym)
    1.17 -  show "transp associated"
    1.18 -    by (rule transpI) (fact associated_trans)
    1.19 -qed
    1.20 -
    1.21  hide_const (open) proj
    1.22  
    1.23  end