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