# HG changeset patch
# User huffman
# Date 1267810067 28800
# Node ID f57de4a9eb9c43fdb18dd1f97f44e24066483947
# Parent  555f26f00e472f7a4900c194256b0cabfc7e100e# Parent  768f8d92b7675cef6a6b8c0c15c802ee6344f184
merged

diff -r 555f26f00e47 -r f57de4a9eb9c src/HOL/Fun.thy
--- 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