HOL Light 2.10 released
 John Harrison
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20051201 (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: http://www.cl.cam.ac.uk/users/jrh/hollight 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