src/HOL/Option.thy
changeset 35719 99b6152aedf5
parent 34886 873c31d9f10d
child 36176 3fe7e97ccca8
--- 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 *}