--- 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
--- 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 *}