src/HOL/Finite_Set.thy

--- a/src/HOL/Finite_Set.thy	Fri Jul 20 00:01:40 2007 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Jul 20 14:27:56 2007 +0200
@@ -7,7 +7,7 @@
 header {* Finite sets *}
 
 theory Finite_Set
-imports Divides Equiv_Relations IntDef
+imports IntDef Divides
 begin
 
 subsection {* Definition and basic properties *}
@@ -94,6 +94,7 @@
   qed
 qed
 
+
 text{* Finite sets are the images of initial segments of natural numbers: *}
 
 lemma finite_imp_nat_seg_image_inj_on: