--- a/src/HOL/Finite_Set.thy Fri Jul 08 11:37:53 2005 +0200
+++ b/src/HOL/Finite_Set.thy Fri Jul 08 11:38:30 2005 +0200
@@ -7,7 +7,7 @@
header {* Finite sets *}
theory Finite_Set
-imports Divides Power Inductive Lattice_Locales
+imports Power Inductive Lattice_Locales
begin
subsection {* Definition and basic properties *}
--- a/src/HOL/PreList.thy Fri Jul 08 11:37:53 2005 +0200
+++ b/src/HOL/PreList.thy Fri Jul 08 11:38:30 2005 +0200
@@ -7,7 +7,7 @@
header{*A Basis for Building the Theory of Lists*}
theory PreList
-imports Wellfounded_Relations Presburger Recdef Relation_Power Parity
+imports Wellfounded_Relations Presburger Relation_Power GCD
begin
text {*