src/HOL/Divides.thy
changeset 47255 30a1692557b0
parent 47217 501b9bbd0d6e
child 47268 262d96552e50
     1.1 --- a/src/HOL/Divides.thy	Sun Apr 01 09:12:03 2012 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sun Apr 01 16:09:58 2012 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* The division operators div and mod *}
     1.5  
     1.6  theory Divides
     1.7 -imports Nat_Numeral Nat_Transfer
     1.8 +imports Nat_Transfer
     1.9  uses "~~/src/Provers/Arith/cancel_div_mod.ML"
    1.10  begin
    1.11