diff -r 58b87aa4dc3b -r 7f7311d04727 src/HOL/BNF/BNF_Def.thy
--- a/src/HOL/BNF/BNF_Def.thy	Mon Jul 15 14:23:51 2013 +0200
+++ b/src/HOL/BNF/BNF_Def.thy	Mon Jul 15 15:50:39 2013 +0200
@@ -17,10 +17,6 @@
 lemma collect_o: "collect F o g = collect ((\<lambda>f. f o g) ` F)"
 by (rule ext) (auto simp only: o_apply collect_def)
 
-lemma converse_mono:
-"R1 ^-1 \<subseteq> R2 ^-1 \<longleftrightarrow> R1 \<subseteq> R2"
-unfolding converse_def by auto
-
 lemma conversep_mono:
 "R1 ^--1 \<le> R2 ^--1 \<longleftrightarrow> R1 \<le> R2"
 unfolding conversep.simps by auto