NEWS
changeset 54587 19cd731eb745
parent 54533 05738b7d8191
child 54588 42b9baf50f8f
equal deleted 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