1.1 --- a/src/HOL/Datatype.thy	Sun Aug 24 14:24:03 2008 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Sun Aug 24 14:42:22 2008 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *}
     1.5  
     1.6  theory Datatype
     1.7 -imports Finite_Set
     1.8 +imports Nat Relation
     1.9  begin
    1.10  
    1.11  typedef (Node)
    1.12 @@ -605,9 +605,6 @@
    1.13  lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
    1.14    by (rule set_ext, case_tac x) auto
    1.15  
    1.16 -instance option :: (finite) finite
    1.17 -  by default (simp add: insert_None_conv_UNIV [symmetric])
    1.18 -
    1.19  
    1.20  subsubsection {* Operations *}
    1.21  

     2.1 --- a/src/HOL/Finite_Set.thy	Sun Aug 24 14:24:03 2008 +0200
     2.2 +++ b/src/HOL/Finite_Set.thy	Sun Aug 24 14:42:22 2008 +0200
     2.3 @@ -7,7 +7,7 @@
     2.4  header {* Finite sets *}
     2.5  
     2.6  theory Finite_Set
     2.7 -imports Divides Transitive_Closure
     2.8 +imports Datatype Divides Transitive_Closure
     2.9  begin
    2.10  
    2.11  subsection {* Definition and basic properties *}
    2.12 @@ -452,9 +452,6 @@
    2.13  instance * :: (finite, finite) finite
    2.14    by default (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
    2.15  
    2.16 -instance "+" :: (finite, finite) finite
    2.17 -  by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
    2.18 -
    2.19  lemma inj_graph: "inj (%f. {(x, y). y = f x})"
    2.20    by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
    2.21  
    2.22 @@ -472,6 +469,12 @@
    2.23    qed
    2.24  qed
    2.25  
    2.26 +instance "+" :: (finite, finite) finite
    2.27 +  by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
    2.28 +
    2.29 +instance option :: (finite) finite
    2.30 +  by default (simp add: insert_None_conv_UNIV [symmetric])
    2.31 +
    2.32  
    2.33  subsection {* A fold functional for finite sets *}
    2.34