| changeset 35580 | 0f74806cab22 |
| parent 35416 | d8d7d1b785af |
| child 35584 | 768f8d92b767 |
--- a/src/HOL/Fun.thy Thu Mar 04 18:42:39 2010 +0100 +++ b/src/HOL/Fun.thy Thu Mar 04 19:43:51 2010 +0100 @@ -378,6 +378,8 @@ apply (simp_all (no_asm_simp) add: inj_image_Compl_subset surj_Compl_image_subset) done +lemma (in ordered_ab_group_add) inj_uminus[iff]: "inj uminus" + by (auto intro!: inj_onI) subsection{*Function Updating*}