# HG changeset patch
# User haftmann
# Date 1219581742 -7200
# Node ID feb0c01cf0fb168f6b6c93afa783d288609383e0
# Parent  5b2c58ab152fa7e87493c4c304abc4cf0aec8c37
tuned import order

diff -r 5b2c58ab152f -r feb0c01cf0fb src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Sun Aug 24 14:24:03 2008 +0200
+++ b/src/HOL/Datatype.thy	Sun Aug 24 14:42:22 2008 +0200
@@ -9,7 +9,7 @@
 header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *}
 
 theory Datatype
-imports Finite_Set
+imports Nat Relation
 begin
 
 typedef (Node)
@@ -605,9 +605,6 @@
 lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
   by (rule set_ext, case_tac x) auto
 
-instance option :: (finite) finite
-  by default (simp add: insert_None_conv_UNIV [symmetric])
-
 
 subsubsection {* Operations *}
 
diff -r 5b2c58ab152f -r feb0c01cf0fb src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sun Aug 24 14:24:03 2008 +0200
+++ b/src/HOL/Finite_Set.thy	Sun Aug 24 14:42:22 2008 +0200
@@ -7,7 +7,7 @@
 header {* Finite sets *}
 
 theory Finite_Set
-imports Divides Transitive_Closure
+imports Datatype Divides Transitive_Closure
 begin
 
 subsection {* Definition and basic properties *}
@@ -452,9 +452,6 @@
 instance * :: (finite, finite) finite
   by default (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
 
-instance "+" :: (finite, finite) finite
-  by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
-
 lemma inj_graph: "inj (%f. {(x, y). y = f x})"
   by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
 
@@ -472,6 +469,12 @@
   qed
 qed
 
+instance "+" :: (finite, finite) finite
+  by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
+
+instance option :: (finite) finite
+  by default (simp add: insert_None_conv_UNIV [symmetric])
+
 
 subsection {* A fold functional for finite sets *}