# HG changeset patch
# User haftmann
# Date 1330289052 -3600
# Node ID 28a01ea3523a2aaecb174d44bc3460fde391fae4
# Parent  b779c3f21f05cf22444b2d3a5140084f11c86bb6
restored accidental omission

diff -r b779c3f21f05 -r 28a01ea3523a src/HOL/Relation.thy
--- 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)