changeset 52730 | 6bf02eb4ddf7 |
parent 52719 | 480a3479fa47 |
child 52731 | dacd47a0633f |
--- a/src/HOL/BNF/BNF_Def.thy Thu Jul 25 08:57:16 2013 +0200 +++ b/src/HOL/BNF/BNF_Def.thy Thu Jul 25 12:25:07 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 conversep_mono: -"R1 ^--1 \<le> R2 ^--1 \<longleftrightarrow> R1 \<le> R2" -unfolding conversep.simps by auto - lemma converse_shift: "R1 \<subseteq> R2 ^-1 \<Longrightarrow> R1 ^-1 \<subseteq> R2" unfolding converse_def by auto