changeset 32010 | cb1a1c94b4cd |
parent 31998 | 2c7a24f74db9 |
child 33274 | b6ff7db522b5 |
--- a/src/HOL/Divides.thy Wed Jul 15 23:11:57 2009 +0200 +++ b/src/HOL/Divides.thy Wed Jul 15 23:48:21 2009 +0200 @@ -655,7 +655,7 @@ in -val cancel_div_mod_nat_proc = Simplifier.simproc (the_context ()) +val cancel_div_mod_nat_proc = Simplifier.simproc @{theory} "cancel_div_mod" ["(m::nat) + n"] (K CancelDivMod.proc); val _ = Addsimprocs [cancel_div_mod_nat_proc];