src/HOL/Relation.thy
changeset 46696 28a01ea3523a
parent 46694 0988b22e2626
child 46752 e9e7209eb375
     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)