Return-Path: Delivery-Date: Received: from lal.cs.byu.edu (actually leopard.cs.byu.edu !OR! info-hol-request@lal.cs.byu.edu) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 16 Sep 1994 11:48:31 +0100 Received: by lal.cs.byu.edu (1.38.193.4/16.2) id AA28646; Fri, 16 Sep 1994 04:36:27 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from gannet.cl.cam.ac.uk by lal.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA28638; Fri, 16 Sep 1994 04:35:03 -0600 Received: from dunlin.cl.cam.ac.uk (user lcp (rfc931)) by gannet.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Fri, 16 Sep 1994 09:59:34 +0100 To: theorem-provers@mc.lcs.mit.edu, info-hol@lal.cs.byu.edu, logic@cs.cornell.edu, bra-types@cs.chalmers.se, isabelle-users@cl.cam.ac.uk Subject: ISABELLE-94 Date: Fri, 16 Sep 94 09:58:07 +0100 From: Lawrence C Paulson Message-Id: <"gannet.cl.ca:072810:940916085943"@cl.cam.ac.uk> ISABELLE-94 We are please to announce a new version of Isabelle. A generic theorem prover, Isabelle supports a classical set theory, a constructive type theory, higher-order logic, modal logics, etc. Isabelle-94 is significantly faster than Isabelle-93. In its higher-order logic and set theory, you can easily make (co)inductive and datatype definitions. In higher-order logic, primitive recursive functions can now be defined directly. In set theory, you can define trees that are infinitely branching or infinitely deep. Isabelle is available by ftp from host ftp.cl.cam.ac.uk, directory ml. Consult the file isabelle.txt for more information on Isabelle and ftp instructions. For Mosaic users, the following URLs are relevant: * for information on Isabelle, open http://www.cl.cam.ac.uk/Research/HVG/isabelle.html * for an index to the Isabelle ftp area, open ftp://ftp.cl.cam.ac.uk/ml/index.html Lawrence C. Paulson Tobias Nipkow Computer Laboratory Institut f|r Informatik University of Cambridge TU M|nchen Cambridge CB2 3QG 80290 M|nchen England Germany Larry.Paulson@cl.cam.ac.uk Tobias.Nipkow@informatik.tu-muenchen.de