minimize imports
authorhuffman
Tue Aug 14 23:04:27 2007 +0200 (2007-08-14)
changeset 242689b4d7c59cc90
parent 24267 867efa1dc4f8
child 24269 4b2aac7669b3
minimize imports
src/HOL/Divides.thy
src/HOL/Finite_Set.thy
     1.1 --- a/src/HOL/Divides.thy	Tue Aug 14 23:03:42 2007 +0200
     1.2 +++ b/src/HOL/Divides.thy	Tue Aug 14 23:04:27 2007 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  header {* The division operators div, mod and the divides relation "dvd" *}
     1.5  
     1.6  theory Divides
     1.7 -imports Datatype Power
     1.8 +imports Power
     1.9  uses "~~/src/Provers/Arith/cancel_div_mod.ML"
    1.10  begin
    1.11  
     2.1 --- a/src/HOL/Finite_Set.thy	Tue Aug 14 23:03:42 2007 +0200
     2.2 +++ b/src/HOL/Finite_Set.thy	Tue Aug 14 23:04:27 2007 +0200
     2.3 @@ -7,7 +7,7 @@
     2.4  header {* Finite sets *}
     2.5  
     2.6  theory Finite_Set
     2.7 -imports IntDef Divides
     2.8 +imports IntDef Divides Datatype
     2.9  begin
    2.10  
    2.11  subsection {* Definition and basic properties *}