--- a/src/HOL/Option.thy Fri Mar 06 20:30:16 2009 +0100
+++ b/src/HOL/Option.thy Fri Mar 06 20:30:17 2009 +0100
@@ -5,7 +5,7 @@
header {* Datatype option *}
theory Option
-imports Datatype
+imports Datatype Finite_Set
begin
datatype 'a option = None | Some 'a
@@ -30,6 +30,9 @@
lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
by (rule set_ext, case_tac x) auto
+instance option :: (finite) finite proof
+qed (simp add: insert_None_conv_UNIV [symmetric])
+
lemma inj_Some [simp]: "inj_on Some A"
by (rule inj_onI) simp