--- a/src/HOL/Fun.thy Fri Mar 05 09:09:11 2010 -0800
+++ b/src/HOL/Fun.thy Fri Mar 05 09:27:47 2010 -0800
@@ -378,9 +378,12 @@
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"
+lemma (in ordered_ab_group_add) inj_uminus[simp, intro]: "inj_on uminus A"
by (auto intro!: inj_onI)
+lemma (in linorder) strict_mono_imp_inj_on: "strict_mono f \<Longrightarrow> inj_on f A"
+ by (auto intro!: inj_onI dest: strict_mono_eq)
+
subsection{*Function Updating*}
definition