| changeset 46165 | 3c5d3d286055 |
| parent 46025 | 66e8a5812f41 |
| child 46574 | c7a13ce60161 |
| 46164:57def0b39696 | 46165:3c5d3d286055 |
|---|---|
94 subsection {* Numeral operations *} |
94 subsection {* Numeral operations *} |
95 |
95 |
96 ML {* |
96 ML {* |
97 structure Dig_Simps = Named_Thms |
97 structure Dig_Simps = Named_Thms |
98 ( |
98 ( |
99 val name = "numeral" |
99 val name = @{binding numeral} |
100 val description = "simplification rules for numerals" |
100 val description = "simplification rules for numerals" |
101 ) |
101 ) |
102 *} |
102 *} |
103 |
103 |
104 setup Dig_Simps.setup |
104 setup Dig_Simps.setup |