src/HOL/Datatype.thy
changeset 27981 feb0c01cf0fb
parent 27823 52971512d1a2
child 28346 b8390cd56b8f
     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