--- 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"