NEWS
 changeset 54587 19cd731eb745 parent 54533 05738b7d8191 child 54588 42b9baf50f8f
equal inserted replaced
54586:ebc8f6bf20c0 54587:19cd731eb745
`    26 `
`    26 `
`    27 * Abolished neg_numeral.`
`    27 * Abolished neg_numeral.`
`    28   * Canonical representation for minus one is "- 1".`
`    28   * Canonical representation for minus one is "- 1".`
`    29   * Canonical representation for other negative numbers is "- (numeral _)".`
`    29   * Canonical representation for other negative numbers is "- (numeral _)".`
`    30   * When devising rule sets for number calculation, consider the`
`    30   * When devising rule sets for number calculation, consider the`
`    31     following cases: 0, 1, numeral _, - 1, - numeral _.`
`    31     following canonical cases: 0, 1, numeral _, - 1, - numeral _.`
`       `
`    32   * HOLogic.dest_number also recognizes numerals in non-canonical forms`
`       `
`    33     like "numeral One", "- numeral One", "- 0" and even "- … - _".`
`    32   * Syntax for negative numerals is mere input syntax.`
`    34   * Syntax for negative numerals is mere input syntax.`
`    33 INCOMPATBILITY.`
`    35 INCOMPATBILITY.`
`    34 `
`    36 `
`    35 * Elimination of fact duplicates:`
`    37 * Elimination of fact duplicates:`
`    36     equals_zero_I ~> minus_unique`
`    38     equals_zero_I ~> minus_unique`