| changeset 32010 | cb1a1c94b4cd |
| parent 31998 | 2c7a24f74db9 |
| child 33274 | b6ff7db522b5 |
| 32009:fd3c60ad9155 | 32010:cb1a1c94b4cd |
|---|---|
653 |
653 |
654 end) |
654 end) |
655 |
655 |
656 in |
656 in |
657 |
657 |
658 val cancel_div_mod_nat_proc = Simplifier.simproc (the_context ()) |
658 val cancel_div_mod_nat_proc = Simplifier.simproc @{theory} |
659 "cancel_div_mod" ["(m::nat) + n"] (K CancelDivMod.proc); |
659 "cancel_div_mod" ["(m::nat) + n"] (K CancelDivMod.proc); |
660 |
660 |
661 val _ = Addsimprocs [cancel_div_mod_nat_proc]; |
661 val _ = Addsimprocs [cancel_div_mod_nat_proc]; |
662 |
662 |
663 end |
663 end |