| changeset 26748 | 4d51ddd6aa5c |
| parent 26300 | 03def556e26e |
| child 27540 | dc38e79f5a1c |
--- a/src/HOL/Divides.thy Thu Apr 24 16:53:04 2008 +0200 +++ b/src/HOL/Divides.thy Fri Apr 25 15:30:33 2008 +0200 @@ -7,7 +7,7 @@ header {* The division operators div, mod and the divides relation dvd *} theory Divides -imports Nat Power Product_Type Wellfounded_Recursion +imports Nat Power Product_Type uses "~~/src/Provers/Arith/cancel_div_mod.ML" begin