# HG changeset patch
# User haftmann
# Date 1163805616 -3600
# Node ID 6aa28caa96c5e4a2dea311adff0bf51a5165d4b3
# Parent  fff1731da03beb48bcab72563bb9f9836ea885f3
clarified module dependencies

diff -r fff1731da03b -r 6aa28caa96c5 src/HOL/Finite_Set.thy
--- 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 *}
diff -r fff1731da03b -r 6aa28caa96c5 src/HOL/Integ/IntDiv.thy
--- 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