From rittinge@informatik.uni-freiburg.de Thu Sep 5 11:46:24 2002 Date: Wed, 14 Aug 2002 08:51:29 +0200 From: Frank Rittinger To: zforum@comlab.ox.ac.uk, czt-project@comlab.ox.ac.uk, isabelle-users@cl.cam.ac.uk, info-hol@ultimate.cs.byu.edu Cc: bkb@informatik.uni-freiburg.de, santen@acm.org, wrwg@microsoft.com Subject: CZT: Announcement: New release of HOL-Z 2.0 [ The following text is in the "iso-8859-1" character set. ] [ Your display is set for the "US-ASCII" character set. Some ] [ characters may be displayed incorrectly. ] *** Announcement of new release: HOL-Z 2.0 *** We are happy to announce the public release of HOL-Z 2.0. HOL-Z is a conservative, structure preserving embedding of Z into the higher-order logic instance of the generic theorem prover Isabelle98. This is a significant update to previous releases of HOL-Z; with - a new LaTex/ZeTa-based front-end, - Automatic generation of refinement proof obligations, - enhanced proof support for mixed Z - and HOL-formulas allowing structured proof in Z, and - an extended set of examples. The sources and installation instructions can be found at the HOL-Z web site at: http://wailoa.informatik.uni-freiburg.de/holz Kind regards, Achim Brucker, Frank Rittinger and Burkhart Wolff *********************************************************************** Frank Rittinger Albert-Ludwigs Universität Freiburg, Institut für Informatik Georges-Koehler-Allee, Geb. 52 (Room 00-021), 79110 Freiburg, Germany Phone: +49 761 203 8245 Fax: +49 761 203 8242 URL: http://www.informatik.uni-freiburg.de/~rittinge *********************************************************************** ----------------------------------------------------------------------- This message is sent to the czt-project mailing list. To join, send an email to czt-project-request@comlab.ox.ac.uk containing the single line subscribe To unsubscribe, do the same, changing the message appropriately. To send a message to the list, write to czt-project@comlab.ox.ac.uk. The CZT home page is at: http://web.comlab.ox.ac.uk/oucl/work/andrew.martin/CZT/ -----------------------------------------------------------------------