From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 03F45BB81 for ; Thu, 1 Dec 2005 07:58:29 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id jB16wSrK010053 for ; Thu, 1 Dec 2005 07:58:28 +0100 Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id HAA29726 for ; Thu, 1 Dec 2005 07:58:27 +0100 (MET) Received: from mta1.cl.cam.ac.uk (mta1.cl.cam.ac.uk [128.232.0.15]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id jB16wReN010050 for ; Thu, 1 Dec 2005 07:58:27 +0100 Received: from nidd.cl.cam.ac.uk ([128.232.8.175] helo=cl.cam.ac.uk ident=[+vin676aTEFT2yYW9tz4V8c/qTHRhaH4]) by mta1.cl.cam.ac.uk with esmtp (Exim 3.092 #1) id 1EhiOc-0000XD-00; Thu, 01 Dec 2005 06:58:22 +0000 X-Uri: To: hol-info@lists.sourceforge.net, caml-list@inria.fr Subject: HOL Light 2.10 released Date: Thu, 01 Dec 2005 06:58:22 +0000 From: John Harrison Message-Id: X-Miltered: at nez-perce with ID 438E9F14.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 438E9F13.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; ocaml:01 bugfixes:01 theorems:01 permutations:01 algebra:01 theorems:01 iter:01 iterated:01 bugfixes:01 trivial:01 sqrt:01 asn:01 bool:01 abstractions:01 verbose:01 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.3 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