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

NEWS

changeset 5541 | f8fb27db4bcd |

parent 5526 | e7617b57a3e6 |

child 5572 | 53c6ea1e6d94 |

1.1 --- a/NEWS Wed Sep 23 10:25:37 1998 +0200 1.2 +++ b/NEWS Wed Sep 23 10:56:08 1998 +0200 1.3 @@ -22,6 +22,10 @@ 1.4 1.5 * HOL: unary - is now overloaded (new type constraints may be required); 1.6 1.7 +* HOL and ZF: unary minus for integers is now #- instead of #~. In ZF, 1.8 + expressions such as n#-1 must be changed to n#- 1, since #-1 is now taken 1.9 + as an integer constant. 1.10 + 1.11 * Pure: ML function 'theory_of' replaced by 'theory'; 1.12 1.13