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

NEWS

changeset 8184 | 6b7ef9fc39da |

parent 8015 | 4a687092b201 |

child 8203 | 2fcc6017cb72 |

1.1 --- a/NEWS Wed Feb 02 12:25:54 2000 +0100 1.2 +++ b/NEWS Wed Feb 02 12:46:57 2000 +0100 1.3 @@ -10,9 +10,17 @@ 1.4 * HOL: the constant for f``x is now "image" rather than "op ``". 1.5 1.6 1.7 +*** Isar *** 1.8 + 1.9 +* names of theorems, assumptions etc. may be natural numbers as well; 1.10 + 1.11 +* new 'obtain' language element supports generalized existence proofs; 1.12 + 1.13 + 1.14 *** HOL *** 1.15 1.16 -* Algebra: new theory of rings and univariate polynomials, by Clemens Ballarin 1.17 +* Algebra: new theory of rings and univariate polynomials, by Clemens 1.18 +Ballarin; 1.19 1.20 1.21