Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
HOL Light 2.10 released
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2005-12-01 (06:58)
From: John Harrison <John.Harrison@c...>
Subject: HOL Light 2.10 released

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

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.


New theorems:

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


    "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


    New subsection of tutorial, plus some minor fixes