| changeset 45607 | 16b4f5774621 |
| parent 45463 | 9a588a835c1e |
| child 47108 | 2a1953f0d20d |
--- a/src/HOL/Numeral_Simprocs.thy Sun Nov 20 21:07:06 2011 +0100 +++ b/src/HOL/Numeral_Simprocs.thy Sun Nov 20 21:07:10 2011 +0100 @@ -14,8 +14,8 @@ ("Tools/nat_numeral_simprocs.ML") begin -declare split_div [of _ _ "number_of k", standard, arith_split] -declare split_mod [of _ _ "number_of k", standard, arith_split] +declare split_div [of _ _ "number_of k", arith_split] for k +declare split_mod [of _ _ "number_of k", arith_split] for k text {* For @{text combine_numerals} *}