src/HOL/Divides.thy
changeset 50422 ee729dbd1b7f
parent 49962 a8cc904a6820
child 51173 3cbb4e95a565
--- a/src/HOL/Divides.thy	Fri Dec 07 14:30:00 2012 +0100
+++ b/src/HOL/Divides.thy	Fri Dec 07 16:25:33 2012 +0100
@@ -9,8 +9,6 @@
 imports Nat_Transfer
 begin
 
-ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
-
 subsection {* Syntactic division operations *}
 
 class div = dvd +