I'm pleased to announce the availability of HOL Light version 2.10 from
the usual Web page:

  http://www.cl.cam.ac.uk/users/jrh/hol-light

There are no very radical changes since 2.00, so existing users needn't
be in any hurry to upgrade. But it now works out of the box under OCaml
3.09, and there are a fair number of worthwhile bugfixes and enhancements,
some of which are listed below.

John.
                                *

New theorems:

    Permutation/*.ml   --- list permutations (thanks to Marco Maggesi)
    Multivariate/*.ml  --- determinants, more linear algebra and integration
    Examples/transc.ml --- many new basic theorems about integrals on R
    Examples/hol88.ml  --- partial HOL88 compatibility file
    Complex/transc.ml  --- some complex transcendental functions
    iter.ml            --- more theorems about iterated operations
    equal.ml           --- PAT_CONV for positional conversion application

Bugfixes:

    "RING" could fail on trivial conclusion with unnecessary hypotheses
    "REAL_RAT_REDUCE_CONV" could leave fractions with denominator 1
    "FIELD" failed to infer nonzeroness of x^n from nonzeroness of x
    "DIFF_CONV" did not cope with sqrt, asn and acs
    "define" had trouble with some functions out of types involving `:bool`
    "define" could not cope with summations in function being defined

Other changes:

    Explicit bound variables in set abstractions (thanks to Sean McLaughlin)
    Universe set on type "ty" can parse and print as "(:ty)"
    MESON is by default less verbose
    Slightly modified lexical conventions for symbols using "," and ";"
    Makefile also works out of the box with newer OCamls

Documentation:

    New subsection of tutorial, plus some minor fixes