# HG changeset patch
# User hoelzl
# Date 1267807750 -3600
# Node ID 768f8d92b7675cef6a6b8c0c15c802ee6344f184
# Parent  c7ddb7105dded178662496efdc6a310f46138f61
generalized inj_uminus; added strict_mono_imp_inj_on

diff -r c7ddb7105dde -r 768f8d92b767 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Fri Mar 05 10:42:13 2010 +0100
+++ b/src/HOL/Fun.thy	Fri Mar 05 17:49:10 2010 +0100
@@ -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