# HG changeset patch
# User nipkow
# Date 1379400171 -7200
# Node ID c5096c22892b7cff3d83c9548608583cfafc021c
# Parent  81e244e71986cf4d0f34204a984f38dd14e3cf16
added lemmas and made concerse executable

diff -r 81e244e71986 -r c5096c22892b src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Tue Sep 17 01:11:37 2013 +0200
+++ b/src/HOL/Relation.thy	Tue Sep 17 08:42:51 2013 +0200
@@ -680,6 +680,12 @@
   "(r\<inverse>\<inverse>)\<inverse>\<inverse> = r"
   by (fact converse_converse [to_pred])
 
+lemma converse_empty[simp]: "{}\<inverse> = {}"
+by auto
+
+lemma converse_UNIV[simp]: "UNIV\<inverse> = UNIV"
+by auto
+
 lemma converse_relcomp: "(r O s)^-1 = s^-1 O r^-1"
   by blast
 
@@ -762,7 +768,7 @@
 lemma conversep_eq [simp]: "(op =)^--1 = op ="
   by (auto simp add: fun_eq_iff)
 
-lemma converse_unfold:
+lemma converse_unfold [code]:
   "r\<inverse> = {(y, x). (x, y) \<in> r}"
   by (simp add: set_eq_iff)