--- a/src/HOL/Library/Cardinality.thy Fri Apr 20 07:36:58 2018 +0000
+++ b/src/HOL/Library/Cardinality.thy Fri Apr 20 07:36:59 2018 +0000
@@ -27,9 +27,6 @@
lemma (in type_definition) card: "card (UNIV :: 'b set) = card A"
by (simp add: univ card_image inj_on_def Abs_inject)
-lemma finite_range_Some: "finite (range (Some :: 'a \<Rightarrow> 'a option)) = finite (UNIV :: 'a set)"
-by(auto dest: finite_imageD intro: inj_Some)
-
lemma infinite_literal: "\<not> finite (UNIV :: String.literal set)"
proof -
have "inj STR" by(auto intro: injI)
--- a/src/HOL/Option.thy Fri Apr 20 07:36:58 2018 +0000
+++ b/src/HOL/Option.thy Fri Apr 20 07:36:59 2018 +0000
@@ -311,6 +311,9 @@
end
+lemma finite_range_Some: "finite (range (Some :: 'a \<Rightarrow> 'a option)) = finite (UNIV :: 'a set)"
+ by (auto dest: finite_imageD intro: inj_Some)
+
subsection \<open>Transfer rules for the Transfer package\<close>