summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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"