# HG changeset patch
# User haftmann
# Date 1439453158 -7200
# Node ID bb3610d34e2e78439df253d5732f4566dfbea6fb
# Parent  141a1d4852595a1fe425f52f8c7f85bd0de4919a
more lemmas

diff -r 141a1d485259 -r bb3610d34e2e src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Aug 13 16:47:00 2015 +0200
+++ b/src/HOL/Fun.thy	Thu Aug 13 10:05:58 2015 +0200
@@ -94,6 +94,14 @@
 lemma bind_image: "Set.bind (f ` A) g = Set.bind A (g \<circ> f)"
 by(auto simp add: Set.bind_def)
 
+lemma (in group_add) minus_comp_minus [simp]:
+  "uminus \<circ> uminus = id"
+  by (simp add: fun_eq_iff)
+
+lemma (in boolean_algebra) minus_comp_minus [simp]:
+  "uminus \<circ> uminus = id"
+  by (simp add: fun_eq_iff)
+
 code_printing
   constant comp \<rightharpoonup> (SML) infixl 5 "o" and (Haskell) infixr 9 "."