src/HOL/Fun.thy
changeset 56154 f0a927235162
parent 56077 d397030fb27e
child 56608 8e3c848008fa
     1.1 --- a/src/HOL/Fun.thy	Sat Mar 15 03:37:22 2014 +0100
     1.2 +++ b/src/HOL/Fun.thy	Sat Mar 15 08:31:33 2014 +0100
     1.3 @@ -72,11 +72,11 @@
     1.4    by clarsimp
     1.5  
     1.6  lemma image_comp:
     1.7 -  "(f o g) ` r = f ` (g ` r)"
     1.8 +  "f ` (g ` r) = (f o g) ` r"
     1.9    by auto
    1.10  
    1.11  lemma vimage_comp:
    1.12 -  "(g \<circ> f) -` x = f -` (g -` x)"
    1.13 +  "f -` (g -` x) = (g \<circ> f) -` x"
    1.14    by auto
    1.15  
    1.16  code_printing
    1.17 @@ -835,8 +835,6 @@
    1.18  lemmas o_eq_elim = comp_eq_elim
    1.19  lemmas o_eq_dest_lhs = comp_eq_dest_lhs
    1.20  lemmas o_eq_id_dest = comp_eq_id_dest
    1.21 -lemmas image_compose = image_comp
    1.22 -lemmas vimage_compose = vimage_comp
    1.23  
    1.24  end
    1.25