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