# HG changeset patch
# User haftmann
# Date 1236367817 -3600
# Node ID 4d1185c77f4ad69aaef2758c470d3e44124ee122
# Parent  a01b2de0e3e1fb052eb82840cf00930d44a39bf5
moved instance option :: finite to Option.thy

diff -r a01b2de0e3e1 -r 4d1185c77f4a src/HOL/Option.thy
--- 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
 
diff -r a01b2de0e3e1 -r 4d1185c77f4a src/HOL/Plain.thy
--- a/src/HOL/Plain.thy	Fri Mar 06 20:30:16 2009 +0100
+++ b/src/HOL/Plain.thy	Fri Mar 06 20:30:17 2009 +0100
@@ -9,9 +9,6 @@
   include @{text Hilbert_Choice}.
 *}
 
-instance option :: (finite) finite
-  by default (simp add: insert_None_conv_UNIV [symmetric])
-
 ML {* path_add "~~/src/HOL/Library" *}
 
 end