--- a/src/HOL/Option.thy Wed Mar 10 08:04:50 2010 +0100
+++ b/src/HOL/Option.thy Wed Mar 10 16:53:27 2010 +0100
@@ -5,7 +5,7 @@
header {* Datatype option *}
theory Option
-imports Datatype Finite_Set
+imports Datatype
begin
datatype 'a option = None | Some 'a
@@ -33,13 +33,6 @@
lemma UNIV_option_conv: "UNIV = insert None (range Some)"
by(auto intro: classical)
-lemma finite_option_UNIV[simp]:
- "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
-by(auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
-
-instance option :: (finite) finite proof
-qed (simp add: UNIV_option_conv)
-
subsubsection {* Operations *}