src/HOL/BNF/BNF_Def.thy
changeset 52749 ed416f4ac34e
parent 52731 dacd47a0633f
child 52986 7f7bbeb16538
     1.1 --- a/src/HOL/BNF/BNF_Def.thy	Sat Jul 27 22:44:04 2013 +0200
     1.2 +++ b/src/HOL/BNF/BNF_Def.thy	Sun Jul 28 12:59:59 2013 +0200
     1.3 @@ -15,15 +15,7 @@
     1.4  begin
     1.5  
     1.6  lemma collect_o: "collect F o g = collect ((\<lambda>f. f o g) ` F)"
     1.7 -by (rule ext) (auto simp only: o_apply collect_def)
     1.8 -
     1.9 -lemma converse_shift:
    1.10 -"R1 \<subseteq> R2 ^-1 \<Longrightarrow> R1 ^-1 \<subseteq> R2"
    1.11 -unfolding converse_def by auto
    1.12 -
    1.13 -lemma conversep_shift:
    1.14 -"R1 \<le> R2 ^--1 \<Longrightarrow> R1 ^--1 \<le> R2"
    1.15 -unfolding conversep.simps by auto
    1.16 +  by (rule ext) (auto simp only: o_apply collect_def)
    1.17  
    1.18  definition convol ("<_ , _>") where
    1.19  "<f , g> \<equiv> %a. (f a, g a)"