src/HOL/Equiv_Relations.thy
changeset 46752 e9e7209eb375
parent 45969 562e99c3d316
child 51112 da97167e03f7
     1.1 --- a/src/HOL/Equiv_Relations.thy	Thu Mar 01 17:13:54 2012 +0000
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Thu Mar 01 19:34:52 2012 +0100
     1.3 @@ -31,7 +31,7 @@
     1.4  
     1.5  lemma sym_trans_comp_subset:
     1.6      "sym r ==> trans r ==> r\<inverse> O r \<subseteq> r"
     1.7 -  by (unfold trans_def sym_def converse_def) blast
     1.8 +  by (unfold trans_def sym_def converse_unfold) blast
     1.9  
    1.10  lemma refl_on_comp_subset: "refl_on A r ==> r \<subseteq> r\<inverse> O r"
    1.11    by (unfold refl_on_def) blast
    1.12 @@ -426,7 +426,7 @@
    1.13  
    1.14  lemma equivp_equiv:
    1.15    "equiv UNIV A \<longleftrightarrow> equivp (\<lambda>x y. (x, y) \<in> A)"
    1.16 -  by (auto intro: equivpI elim: equivpE simp add: equiv_def reflp_def symp_def transp_def)
    1.17 +  by (auto intro!: equivI equivpI [to_set] elim!: equivE equivpE [to_set])
    1.18  
    1.19  lemma equivp_reflp_symp_transp:
    1.20    shows "equivp R \<longleftrightarrow> reflp R \<and> symp R \<and> transp R"
    1.21 @@ -449,3 +449,4 @@
    1.22    by (erule equivpE, erule transpE)
    1.23  
    1.24  end
    1.25 +