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