changeset 32010 | cb1a1c94b4cd |
parent 31998 | 2c7a24f74db9 |
child 32075 | e8e0fb5da77a |
--- a/src/HOL/IntDiv.thy Wed Jul 15 23:11:57 2009 +0200 +++ b/src/HOL/IntDiv.thy Wed Jul 15 23:48:21 2009 +0200 @@ -266,7 +266,7 @@ in -val cancel_div_mod_int_proc = Simplifier.simproc (the_context ()) +val cancel_div_mod_int_proc = Simplifier.simproc @{theory} "cancel_zdiv_zmod" ["(k::int) + l"] (K CancelDivMod.proc); val _ = Addsimprocs [cancel_div_mod_int_proc];