--- a/src/HOL/Finite_Set.thy Sat Nov 18 00:20:15 2006 +0100
+++ b/src/HOL/Finite_Set.thy Sat Nov 18 00:20:16 2006 +0100
@@ -7,7 +7,7 @@
header {* Finite sets *}
theory Finite_Set
-imports Power Inductive Lattices
+imports Power Divides Inductive Lattices
begin
subsection {* Definition and basic properties *}
--- a/src/HOL/Integ/IntDiv.thy Sat Nov 18 00:20:15 2006 +0100
+++ b/src/HOL/Integ/IntDiv.thy Sat Nov 18 00:20:16 2006 +0100
@@ -9,7 +9,7 @@
header{*The Division Operators div and mod; the Divides Relation dvd*}
theory IntDiv
-imports "../SetInterval" "../Recdef"
+imports "../Divides" "../SetInterval" "../Recdef"
uses ("IntDiv_setup.ML")
begin