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

NEWS

changeset 5282 | 80c75c862a8f |

parent 5275 | de5d5e5eb692 |

child 5308 | 3ca4da83012c |

1.1 --- a/NEWS Sat Aug 08 14:00:56 1998 +0200 1.2 +++ b/NEWS Sat Aug 08 14:12:25 1998 +0200 1.3 @@ -202,8 +202,10 @@ 1.4 1.5 * HOL/Vimage: new theory for inverse image of a function, syntax f-``B; 1.6 1.7 -* HOL/List: new function list_update written xs[i:=v] that updates the i-th 1.8 - list position. May also be iterated as in xs[i:=a,j:=b,...]. 1.9 +* HOL/List: 1.10 + - new function list_update written xs[i:=v] that updates the i-th 1.11 + list position. May also be iterated as in xs[i:=a,j:=b,...]. 1.12 + - new lexicographic orderings and corresponding wellfoundedness theorems. 1.13 1.14 * HOL/Arith: 1.15 - removed 'pred' (predecessor) function;