1.1 --- a/src/HOL/Divides.thy Wed Feb 27 20:36:21 2013 +0100
1.2 +++ b/src/HOL/Divides.thy Thu Feb 28 11:40:23 2013 +0100
1.3 @@ -686,6 +686,8 @@
1.4
1.5 text {* Simproc for cancelling @{const div} and @{const mod} *}
1.6
1.7 +ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
1.8 +
1.9 ML {*
1.10 structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
1.11 (
2.1 --- a/src/HOL/Nat_Transfer.thy Wed Feb 27 20:36:21 2013 +0100
2.2 +++ b/src/HOL/Nat_Transfer.thy Thu Feb 28 11:40:23 2013 +0100
2.3 @@ -420,8 +420,4 @@
2.4 return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
2.5 cong: setsum_cong setprod_cong]
2.6
2.7 -
2.8 -(*belongs to Divides.thy, but slows down dependency discovery*)
2.9 -ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
2.10 -
2.11 end