changeset 52660 | 7f7311d04727 |
parent 52659 | 58b87aa4dc3b |
child 52719 | 480a3479fa47 |
--- 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