# HG changeset patch
# User haftmann
# Date 1295599452 -3600
# Node ID 89451110ba8e0dccd9d85f4bc01e8dd135d6688c
# Parent  011fcb70e32f433097371abeff78daa75c2a3297
moved theorem

diff -r 011fcb70e32f -r 89451110ba8e src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Jan 21 09:41:59 2011 +0100
+++ b/src/HOL/Finite_Set.thy	Fri Jan 21 09:44:12 2011 +0100
@@ -9,15 +9,6 @@
 imports Option Power
 begin
 
--- {* FIXME move *}
-
-lemma inj_vimage_singleton: "inj f \<Longrightarrow> f -` {a} \<subseteq> {THE x. f x = a}"
-  -- {* The inverse image of a singleton under an injective function
-         is included in a singleton. *}
-  apply (auto simp add: inj_on_def)
-  apply (blast intro: the_equality [symmetric])
-  done
-
 subsection {* Predicate for finite sets *}
 
 inductive finite :: "'a set \<Rightarrow> bool"
diff -r 011fcb70e32f -r 89451110ba8e src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Fri Jan 21 09:41:59 2011 +0100
+++ b/src/HOL/Fun.thy	Fri Jan 21 09:44:12 2011 +0100
@@ -546,12 +546,20 @@
 apply (simp_all (no_asm_simp) add: inj_image_Compl_subset surj_Compl_image_subset)
 done
 
+lemma inj_vimage_singleton: "inj f \<Longrightarrow> f -` {a} \<subseteq> {THE x. f x = a}"
+  -- {* The inverse image of a singleton under an injective function
+         is included in a singleton. *}
+  apply (auto simp add: inj_on_def)
+  apply (blast intro: the_equality [symmetric])
+  done
+
 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