restored accidental omission

--- a/src/HOL/Relation.thy	Sun Feb 26 21:43:57 2012 +0100
+++ b/src/HOL/Relation.thy	Sun Feb 26 21:44:12 2012 +0100
@@ -512,8 +512,7 @@
 
 lemma conversep_converse_eq [pred_set_conv]:
   "(\<lambda>x y. (x, y) \<in> r)^--1 = (\<lambda>x y. (x, y) \<in> r^-1)"
-  apply (auto simp add: fun_eq_iff)
-  oops
+  by (auto simp add: fun_eq_iff)
 
 lemma conversep_conversep [simp]: "(r^--1)^--1 = r"
   by (iprover intro: order_antisym conversepI dest: conversepD)