more lemmas
authorhaftmann
Thu Aug 13 10:05:58 2015 +0200 (2015-08-13)
changeset 60929bb3610d34e2e
parent 60928 141a1d485259
child 60930 dd8ab7252ba2
more lemmas
src/HOL/Fun.thy
     1.1 --- a/src/HOL/Fun.thy	Thu Aug 13 16:47:00 2015 +0200
     1.2 +++ b/src/HOL/Fun.thy	Thu Aug 13 10:05:58 2015 +0200
     1.3 @@ -94,6 +94,14 @@
     1.4  lemma bind_image: "Set.bind (f ` A) g = Set.bind A (g \<circ> f)"
     1.5  by(auto simp add: Set.bind_def)
     1.6  
     1.7 +lemma (in group_add) minus_comp_minus [simp]:
     1.8 +  "uminus \<circ> uminus = id"
     1.9 +  by (simp add: fun_eq_iff)
    1.10 +
    1.11 +lemma (in boolean_algebra) minus_comp_minus [simp]:
    1.12 +  "uminus \<circ> uminus = id"
    1.13 +  by (simp add: fun_eq_iff)
    1.14 +
    1.15  code_printing
    1.16    constant comp \<rightharpoonup> (SML) infixl 5 "o" and (Haskell) infixr 9 "."
    1.17