| changeset 51299 | 30b014246e21 |
| parent 51173 | 3cbb4e95a565 |
| child 51717 | 9e7d1c139569 |
--- a/src/HOL/Divides.thy Wed Feb 27 20:36:21 2013 +0100 +++ b/src/HOL/Divides.thy Thu Feb 28 11:40:23 2013 +0100 @@ -686,6 +686,8 @@ text {* Simproc for cancelling @{const div} and @{const mod} *} +ML_file "~~/src/Provers/Arith/cancel_div_mod.ML" + ML {* structure Cancel_Div_Mod_Nat = Cancel_Div_Mod (