src/HOL/Fun.thy
changeset 60929 bb3610d34e2e
parent 60758 d8d85a8172b5
child 61204 3e491e34a62e
     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