NEWS
changeset 30562 7b0017587e7d
parent 30547 4c2514625873
child 30577 79cc595655c0
     1.1 --- a/NEWS	Mon Mar 16 15:10:59 2009 -0700
     1.2 +++ b/NEWS	Mon Mar 16 15:58:41 2009 -0700
     1.3 @@ -211,6 +211,25 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Theory Library/Polynomial.thy defines an abstract type 'a poly of
     1.8 +univariate polynomials with coefficients of type 'a.  In addition to
     1.9 +the standard ring operations, it also supports div and mod.  Code
    1.10 +generation is also supported, using list-style constructors.
    1.11 +
    1.12 +* Theory Library/Inner_Product.thy defines a class of real_inner for
    1.13 +real inner product spaces, with an overloaded operation inner :: 'a =>
    1.14 +'a => real.  Class real_inner is a subclass of real_normed_vector from
    1.15 +RealVector.thy.
    1.16 +
    1.17 +* Theory Library/Product_Vector.thy provides instances for the product
    1.18 +type 'a * 'b of several classes from RealVector.thy and
    1.19 +Inner_Product.thy.  Definitions of addition, subtraction, scalar
    1.20 +multiplication, norms, and inner products are included.
    1.21 +
    1.22 +* Theory Library/Bit.thy defines the field "bit" of integers modulo 2.
    1.23 +In addition to the field operations, numerals and case syntax are also
    1.24 +supported.
    1.25 +
    1.26  * Theory Library/Diagonalize.thy provides constructive version of
    1.27  Cantor's first diagonalization argument.
    1.28  
    1.29 @@ -241,7 +260,7 @@
    1.30  * Common decision procedures (Cooper, MIR, Ferrack, Approximation, Dense_Linear_Order)
    1.31  now in directory HOL/Decision_Procs.
    1.32  
    1.33 -* Theory HOL/Decisioin_Procs/Approximation.thy provides the new proof method
    1.34 +* Theory HOL/Decision_Procs/Approximation.thy provides the new proof method
    1.35  "approximation".  It proves formulas on real values by using interval arithmetic.
    1.36  In the formulas are also the transcendental functions sin, cos, tan, atan, ln,
    1.37  exp and the constant pi are allowed. For examples see