# HG changeset patch
# User huffman
# Date 1187125467 -7200
# Node ID 9b4d7c59cc906c639ebc2d54936c5aed1d2990e6
# Parent  867efa1dc4f8192cecf133c758e2e8501cac7d0d
minimize imports

diff -r 867efa1dc4f8 -r 9b4d7c59cc90 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue Aug 14 23:03:42 2007 +0200
+++ b/src/HOL/Divides.thy	Tue Aug 14 23:04:27 2007 +0200
@@ -7,7 +7,7 @@
 header {* The division operators div, mod and the divides relation "dvd" *}
 
 theory Divides
-imports Datatype Power
+imports Power
 uses "~~/src/Provers/Arith/cancel_div_mod.ML"
 begin
 
diff -r 867efa1dc4f8 -r 9b4d7c59cc90 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Aug 14 23:03:42 2007 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Aug 14 23:04:27 2007 +0200
@@ -7,7 +7,7 @@
 header {* Finite sets *}
 
 theory Finite_Set
-imports IntDef Divides
+imports IntDef Divides Datatype
 begin
 
 subsection {* Definition and basic properties *}