equal
deleted
inserted
replaced
142 code_datatype "number_of \<Colon> int \<Rightarrow> code_numeral" |
142 code_datatype "number_of \<Colon> int \<Rightarrow> code_numeral" |
143 |
143 |
144 |
144 |
145 subsection {* Basic arithmetic *} |
145 subsection {* Basic arithmetic *} |
146 |
146 |
147 instantiation code_numeral :: "{minus, ordered_semidom, semiring_div, linorder}" |
147 instantiation code_numeral :: "{minus, linordered_semidom, semiring_div, linorder}" |
148 begin |
148 begin |
149 |
149 |
150 definition [simp, code del]: |
150 definition [simp, code del]: |
151 "(1\<Colon>code_numeral) = of_nat 1" |
151 "(1\<Colon>code_numeral) = of_nat 1" |
152 |
152 |