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

NEWS

changeset 14610 | 9c2e31e483b2 |

parent 14606 | 0be6c11e7128 |

child 14624 | 9b3397a848c3 |

1.1 --- a/NEWS Fri Apr 16 21:03:40 2004 +0200 1.2 +++ b/NEWS Sat Apr 17 00:46:22 2004 +0200 1.3 @@ -143,7 +143,10 @@ 1.4 * HOL-Algebra: new locale "ring" for non-commutative rings. 1.5 1.6 * HOL-ex: InductiveInvariant_examples illustrates advanced recursive function 1.7 - defintions, thanks to Sava Krsti\'{c} and John Matthews. 1.8 + definitions, thanks to Sava Krsti\'{c} and John Matthews. 1.9 + 1.10 +* HOL-Matrix: a first theory for matrices in HOL with an application of 1.11 + matrix theory to linear programming. 1.12 1.13 * Unions and Intersections: 1.14 The x-symbol output syntax of UN and INT has been changed