src/HOL/Fun.thy
changeset 35584 768f8d92b767
parent 35580 0f74806cab22
child 36176 3fe7e97ccca8
     1.1 --- a/src/HOL/Fun.thy	Fri Mar 05 10:42:13 2010 +0100
     1.2 +++ b/src/HOL/Fun.thy	Fri Mar 05 17:49:10 2010 +0100
     1.3 @@ -378,9 +378,12 @@
     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 +lemma (in ordered_ab_group_add) inj_uminus[simp, intro]: "inj_on uminus A"
     1.9    by (auto intro!: inj_onI)
    1.10  
    1.11 +lemma (in linorder) strict_mono_imp_inj_on: "strict_mono f \<Longrightarrow> inj_on f A"
    1.12 +  by (auto intro!: inj_onI dest: strict_mono_eq)
    1.13 +
    1.14  subsection{*Function Updating*}
    1.15  
    1.16  definition