English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

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/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


    "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