equal
deleted
inserted
replaced
208 |
208 |
209 - replace "#nnn" by "nnn", and "#-nnn" by "-nnn"; |
209 - replace "#nnn" by "nnn", and "#-nnn" by "-nnn"; |
210 |
210 |
211 - remove all special provisions on numerals in proofs; |
211 - remove all special provisions on numerals in proofs; |
212 |
212 |
213 * HOL: simp rules nat_number_of expand numerals on nat to Suc/0 |
213 * HOL: simp rules nat_number expand numerals on nat to Suc/0 |
214 representation (depends on bin_arith_simps in the default context); |
214 representation (depends on bin_arith_simps in the default context); |
215 |
215 |
216 * HOL: symbolic syntax for x^2 (numeral 2); |
216 * HOL: symbolic syntax for x^2 (numeral 2); |
217 |
217 |
218 * HOL: the class of all HOL types is now called "type" rather than |
218 * HOL: the class of all HOL types is now called "type" rather than |