author | paulson |

Wed Sep 23 10:56:08 1998 +0200 (1998-09-23) | |

changeset 5541 | f8fb27db4bcd |

parent 5540 | 0f16c3b66ab4 |

child 5542 | f0c303f53730 |

unary minus

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