diff -r 564ea783ace8 -r a010aab5bed0 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Jan 21 23:40:23 2009 +0100
+++ b/src/HOL/Finite_Set.thy	Wed Jan 21 23:40:23 2009 +0100
@@ -6,7 +6,7 @@
 header {* Finite sets *}
 
 theory Finite_Set
-imports Datatype Divides Transitive_Closure
+imports Nat Product_Type Power
 begin
 
 subsection {* Definition and basic properties *}
@@ -380,46 +380,6 @@
 by(blast intro: finite_subset[OF subset_Pow_Union])
 
 
-lemma finite_converse [iff]: "finite (r^-1) = finite r"
-  apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
-   apply simp
-   apply (rule iffI)
-    apply (erule finite_imageD [unfolded inj_on_def])
-    apply (simp split add: split_split)
-   apply (erule finite_imageI)
-  apply (simp add: converse_def image_def, auto)
-  apply (rule bexI)
-   prefer 2 apply assumption
-  apply simp
-  done
-
-
-text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi
-Ehmety) *}
-
-lemma finite_Field: "finite r ==> finite (Field r)"
-  -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
-  apply (induct set: finite)
-   apply (auto simp add: Field_def Domain_insert Range_insert)
-  done
-
-lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r"
-  apply clarify
-  apply (erule trancl_induct)
-   apply (auto simp add: Field_def)
-  done
-
-lemma finite_trancl: "finite (r^+) = finite r"
-  apply auto
-   prefer 2
-   apply (rule trancl_subset_Field2 [THEN finite_subset])
-   apply (rule finite_SigmaI)
-    prefer 3
-    apply (blast intro: r_into_trancl' finite_subset)
-   apply (auto simp add: finite_Field)
-  done
-
-
 subsection {* Class @{text finite}  *}
 
 setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
@@ -471,9 +431,6 @@
 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 *}