equal
deleted
inserted
replaced
182 |
182 |
183 - replace "#nnn" by "nnn", and "#-nnn" by "-nnn"; |
183 - replace "#nnn" by "nnn", and "#-nnn" by "-nnn"; |
184 |
184 |
185 - remove all special provisions on numerals in proofs; |
185 - remove all special provisions on numerals in proofs; |
186 |
186 |
|
187 * HOL: simp rules nat_number_of expand numerals on nat to Suc/0 |
|
188 representation (depends on bin_arith_simps in the default context); |
|
189 |
187 * HOL: symbolic syntax for x^2 (numeral 2); |
190 * HOL: symbolic syntax for x^2 (numeral 2); |
188 |
191 |
189 * HOL: the class of all HOL types is now called "type" rather than |
192 * HOL: the class of all HOL types is now called "type" rather than |
190 "term"; INCOMPATIBILITY, need to adapt references to this type class |
193 "term"; INCOMPATIBILITY, need to adapt references to this type class |
191 in axclass/classes, instance/arities, and (usually rare) occurrences |
194 in axclass/classes, instance/arities, and (usually rare) occurrences |