[Prev][Next][Index][Thread]

ISABELLE-91

Date: Thu, 29 Aug 91 15:56:21 +0100

			       ISABELLE-91
		          (Second Beta-Release)

We are pleased to announce a new version of Isabelle supporting
"Order-Sorted Polymorphism".  This type system lies between that of ML and
Haskell and allows the definition of polymorphic object-logics with
automatic type inference.  Higher-order logic, similar to that of the
Cambridge HOL system, is now an Isabelle object-logic.  Isabelle's
First-order logic is now many-sorted, with polymorphic quantifiers and
equality.

A new rewriting package is now available.  It can be instantiated to any
reflexive/transitive relation (such as = and <->) for which congruence
rules can be proved.  It handles conditional rewrite rules by a recursive
invocation of rewriting.  It also supports contextual extraction of rewrite
rules -- for example, rewriting the formula x=a --> P(x) to x=a --> P(a).

A number of smaller changes simplify the definition of new logics.
Isabelle's Zermelo-Fraenkel set theory now derives a theory of functions,
transfinite recursion, and several recursive data structures (including
mutually recursive trees and forests).  Several forms of modal logic are
now available.

The new release is NOT upwards compatible with previous ones.  Most changes
are (inadequately!) documented in an addition to the manual.  Modifications
of existing logic definitions and tactics should be fairly minor.

Isabelle is a generic theorem prover, and comes with seven different
object-logics.  New logics are introduced by specifying their syntax and
rules of inference.  Proof procedures are expressed using Standard ML.  A
manual is distributed as LaTeX sources; the following article gives a brief
introduction to Isabelle:

    L. C. Paulson, Isabelle: The next 700 theorem provers,
    In: P. Odifreddi (editor), Logic and Computer Science
    (Academic Press, 1990), 361-385.

---------------------------------------------------------------------------

Isabelle-91 is available by anonymous ftp from the University of Cambridge.
Instructions:

  * Connect to host ftp.cl.cam.ac.uk [Internet address: 128.232.0.57]
  * Use login id "anonymous" with your name as password
  * put ftp in BINARY MODE ("binary") 
  * go to directory ml (by typing "cd ml")
  * "get" the file isabelle.tar.Z in that directory.  

Here is a sample dialog:

   ftp
   ftp> open ftp.cl.cam.ac.uk
   Name: anonymous
   Password: <your name>
   ftp> binary
   ftp> cd ml
   ftp> get isabelle.tar.Z
   ftp> close
   ftp> quit

Once transferred, the file should be uncompressed using the uncompress
command, then extracted using tar:

   uncompress -c isabelle.tar.Z | tar xf -

This will add a directory called 91 (for Isabelle-91) to the current
directory.  The new directory should contain around 30 files, including 10
subdirectories.  Its total size is under 1.6 megabytes.

The file COPYRIGHT contains the Copyright notice and Disclaimer of Warranty.

The file README contains instructions for compiling Isabelle.

---------------------------------------------------------------------------

Tobias Nipkow 		  		E-mail: Tobias.Nipkow@cl.cam.ac.uk 
Lawrence C Paulson			E-mail: Larry.Paulson@cl.cam.ac.uk 

Computer Laboratory 			Phone: +44-223-334600
University of Cambridge 		Fax:   +44-223-334678
Pembroke Street 
Cambridge CB2 3QG 
England