src/HOL/Divides.thy
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