Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: info-hol@leopard.cs.byu.edu
Subject: Release notes for hol90, version 7
Message-Id: <94Nov10.123410met.8082@sunbroy14.informatik.tu-muenchen.de>
Date: Thu, 10 Nov 1994 12:34:03 +0100


            HOL90 VERSION 7 RELEASE NOTES

The following is a quick overview of some interesting additions to the
system.


Organization and Documentation.
-------------------------------

* The loose assortment of documentation for hol90 has been improved and
  stitched together using HTML. The master document can be found in
  doc/manual.html.

* A new directory, called "examples", has been added at the top level
  of the hol90 directory hierarchy.

* There is an analogue of "print_theory" which generates HTML, including
  hyperlinks to parent theories. This has been used to (nearly 
  automatically) generate a "map" to all theories that come bundled with 
  the hol90 distribution. This guide is locally accessible (through a
  hyperlink in the manual), or remotely via the hyperlinks

    (Europe)
    ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/slind/hol90/contrib/map/MAP.html
    or
    (North America)
    ftp://ftp.research.att.com/dist/ml/hol90/contrib/map/MAP.html


Core Functionality.
---------------------

* A number of minor bugs (mostly in the prettyprinter) have been fixed.
  Some new flags have also been introduced to control some facets of
  prettyprinting. For example, infixes have traditionally printed at
  the ends of lines; now with the flip of a switch, one can have a
  Lamportesque view of HOL types, terms, goals, and theorems.

* Richard Boulton has made the prettyprinter extensible.

* Support for restricted binders has been added.

* The implementation of rewriting now uses an abstract type of 
  rewrite-rule sets. The constituents of such rulesets are visible, 
  thanks to a custom prettyprinter.

* A more detailed "theorem-counting" facility has been added. Now,
  separate counts are kept for each primitive rule; for the derived
  rules; when definitions and axioms are built; when a theorem is 
  loaded in from disk; when theorems are made when checking for
  validity of tactics; and finally for anytime the user just makes a
  theorem.

* The code component of libraries can load faster. The code loaded will, 
  however, run slower.

* The goalstack has been spruced up a bit. For example, the display of 
  goals is programmable.


Libraries.
-------------

There are more libraries and they have better documentation.
Some new system libraries are available:

    * "pair"             - Extension of various facilities to products
    * "real"             - Development of real numbers and analysis
    * "wellorder"        - Wellorderings and versions of the Axiom of Choice
    * "list"             - Further development of lists
    * "window inference" - A refinement-style proof manager
    * "res_quan"         - Support for restricted quantification
    * "word"             - Bitstrings


In contrib there a number of interesting additions:

    * "fixpoint"         - Scott's fixpoint theory
    * "CSP"              - Hoare's Communicating Sequential Processes
    * "generator"        - Support for constructing "deep" embeddings
    * "cond"             - Support for conditional expressions
    * "more_utils"       - Miscellaneous proof support
    * "pev_rewrite"      - "partial-evaluation technology" rewriter-generator
    * "mutrec"           - Mutually recursive datatype definitions
    * "nested_rec"       - Nested recursive datatype definitions
    * "orsml"            - A database query language applied to theories
    * "part_fun"         - Support for partial functions
    * "holML"            - The dynamic semantics of SML, including HO functors
    * "map"              - An HTML guide to all theories in the distribution


Jim Grundy, David Shepherd, John Harrison, Chris Toshok, Wai Wong, Paul
Curzon, Mike Gordon, Albert Camilleri, Brian Graham, Morten Welinder,
Ralph Reetz, Elsa Gunter, Healfdene Goguen, Leonid Libkin, Savi Maharaj,
and Myra VanInwegen have been involved in either authoring or porting
the above libraries.


Konrad.