NEWS
changeset 11702 ebfe5ba905b0
parent 11700 a0e6bda62b7b
child 11712 deb8cac87063
     1.1 --- a/NEWS	Fri Oct 05 21:52:39 2001 +0200
     1.2 +++ b/NEWS	Fri Oct 05 23:58:17 2001 +0200
     1.3 @@ -33,6 +33,32 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* HOL: moved over to sane numeral syntax; the new policy is as
     1.8 +follows:
     1.9 +
    1.10 +  - 0 and 1 are polymorphic constants, which are defined on any
    1.11 +  numeric type (nat, int, real etc.);
    1.12 +
    1.13 +  - 2, 3, 4, ... and -1, -2, -3, ... are polymorphic numerals, based
    1.14 +  binary representation internally;
    1.15 +
    1.16 +  - type nat has special constructor Suc, and generally prefers Suc 0
    1.17 +  over 1::nat and Suc (Suc 0) over 2::nat;
    1.18 +
    1.19 +This change may cause significant INCOMPATIBILITIES; here are some
    1.20 +hints on converting existing sources:
    1.21 +
    1.22 +  - due to the new "num" token, "-0" and "-1" etc. are now atomic
    1.23 +  entities, so expressions involving "-" (unary or binary minus) need
    1.24 +  to be spaced properly;
    1.25 +
    1.26 +  - existing occurrences of "1" may need to be constraint "1::nat" or
    1.27 +  even replaced by Suc 0; similar for old "2";
    1.28 +
    1.29 +  - replace "#nnn" by "nnn", and "#-nnn" by "-nnn";
    1.30 +
    1.31 +  - remove all special provisions on numerals in proofs;
    1.32 +
    1.33  * HOL: linorder_less_split superseded by linorder_cases;
    1.34  
    1.35  * HOL: added "The" definite description operator; move Hilbert's "Eps"