restored accidental omission
authorhaftmann
Sun Feb 26 21:44:12 2012 +0100 (2012-02-26)
changeset 4669628a01ea3523a
parent 46695 b779c3f21f05
child 46697 b07ae33cc459
child 46724 5759ecd5c905
restored accidental omission
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Relation.thy	Sun Feb 26 21:43:57 2012 +0100
     1.2 +++ b/src/HOL/Relation.thy	Sun Feb 26 21:44:12 2012 +0100
     1.3 @@ -512,8 +512,7 @@
     1.4  
     1.5  lemma conversep_converse_eq [pred_set_conv]:
     1.6    "(\<lambda>x y. (x, y) \<in> r)^--1 = (\<lambda>x y. (x, y) \<in> r^-1)"
     1.7 -  apply (auto simp add: fun_eq_iff)
     1.8 -  oops
     1.9 +  by (auto simp add: fun_eq_iff)
    1.10  
    1.11  lemma conversep_conversep [simp]: "(r^--1)^--1 = r"
    1.12    by (iprover intro: order_antisym conversepI dest: conversepD)