src/HOL/BNF_Comp.thy
changeset 55066 4e5ddf3162ac
parent 55062 6d3fad6f01c9
child 55705 a98a045a6169
     1.1 --- a/src/HOL/BNF_Comp.thy	Mon Jan 20 18:24:56 2014 +0100
     1.2 +++ b/src/HOL/BNF_Comp.thy	Mon Jan 20 18:24:56 2014 +0100
     1.3 @@ -15,10 +15,10 @@
     1.4  by (rule ext) simp
     1.5  
     1.6  lemma Union_natural: "Union o image (image f) = image f o Union"
     1.7 -by (rule ext) (auto simp only: o_apply)
     1.8 +by (rule ext) (auto simp only: comp_apply)
     1.9  
    1.10  lemma in_Union_o_assoc: "x \<in> (Union o gset o gmap) A \<Longrightarrow> x \<in> (Union o (gset o gmap)) A"
    1.11 -by (unfold o_assoc)
    1.12 +by (unfold comp_assoc)
    1.13  
    1.14  lemma comp_single_set_bd:
    1.15    assumes fbd_Card_order: "Card_order fbd" and
    1.16 @@ -58,7 +58,7 @@
    1.17  by blast
    1.18  
    1.19  lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>((\<lambda>f. f x) ` X)| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
    1.20 -by (unfold o_apply collect_def SUP_def)
    1.21 +by (unfold comp_apply collect_def SUP_def)
    1.22  
    1.23  lemma wpull_cong:
    1.24  "\<lbrakk>A' = A; B1' = B1; B2' = B2; wpull A B1 B2 f1 f2 p1 p2\<rbrakk> \<Longrightarrow> wpull A' B1' B2' f1 f2 p1 p2"