diff -r 204f4ebbba64 -r 85539b33be03 README.html --- a/README.html Fri May 05 22:18:40 2000 +0200 +++ b/README.html Fri May 05 22:23:27 2000 +0200 @@ -1,4 +1,3 @@ - @@ -25,7 +24,7 @@ starts at about 32-64 MB of free main memory (somewhat depending on your ML system), with several tens of MB disk space and a decent CPU. Speaking by today's hardware standards, any moderate Linux box should -make a nice platform for Isabelle. +give a very nice platform for Isabelle.

@@ -43,38 +42,38 @@ The following ML system and platform combinations are known to work very well:

Poly/ML 3.x on Linux and Suns. -
SML/NJ 110.x on any Unix platform (e.g. Linux, Suns). +
Poly/ML 3.x on Linux and Sparc/Solaris. +
SML/NJ 110.x on any Unix platform (Linux, Suns, SGI etc.).
SML/NJ 0.93 on Suns and SGIs. There seem to be several problems with Linux and HP-UX, though.

Poly/ML, previously a commercial -product, is back in the public domain. It is the best compiler for running -Isabelle, requiring the least memory and offering the fastest performance. +

Poly/ML, previously a +commercial product, is back in the free world. It is by far the best +compiler for running Isabelle, requiring the least memory and offering +the highest performance.

SML/NJ -needs lots of store and disk space, but it is free. The current -official release is 110 (there is an RPM -archive available for Linux/x86). We still support the old 0.93 -release, but do not recommend it. +needs lots of store and disk space, but supports many more platforms. +The current official release is 110. Basically, we still support the +old 0.93 release, but do not recommend it. -

MLWorks is a commercial ML programming environment developed by -Harlequin and was -unfortunately withdrawn after that company was taken over. Isabelle on -MLWorks 2.0 works well. It is about 20% faster than on SML/NJ while using -slightly less memory and disk space. A few minor features (e.g. ML top-level -pretty printing) are not supported, though. - +

MLWorks is a commercial ML programming environment developed by Harlequin and was unfortunately +withdrawn after that company was taken over. Isabelle on MLWorks 2.0 +works well. It is about 20% faster than on SML/NJ while using +slightly less memory and disk space. A few minor features (e.g. ML +top-level pretty printing) are not supported, though.

Installation

-Binary rpm packages are available for Isabelle/HOL and ZF on the -Linux/x86 platform. Alternatively, the system may be built from -scratch as described in file INSTALL of the Isabelle sources. +RPM packages are available for Isabelle/HOL and ZF on the Linux/x86 +platform. The system may be easily built from scratch as well, taking +the traditional tar.gz distribution. See file INSTALL as +distributed with Isabelle for more information. + Further background information may be found in the Isabelle System Manual, distributed with the sources (directory doc). @@ -82,33 +81,51 @@

User interfaces

The distribution includes only a very primitive interface based on -ordinary terminal sessions. Advanced interfaces are available from +ordinary terminal sessions. Advanced interfaces are available from other sources: -

-Isamode by -David Aspinall is a more elaborate interface for Isabelle. It runs -under recent versions of XEmacs and is useful to both novices and -experts. +
- -Proof General is -a generic Emacs interface for proof assistants, including Isabelle -(both for the classic and Isar version). Proof General is suitable -for use by pacifists and Emacs militants alike. Its most prominent -feature is script management, providing a metaphor of live proof -script editing. -
+
+Proof General by +David Aspinall and others is a generic Emacs interface for proof +assistants, including Isabelle (both for the classic and Isar +version). Proof General is suitable for use by pacifists and Emacs +militants alike. Its most prominent feature is script management, +providing a metaphor of live proof script editing. Proof +General has recently gained a rather large following of both beginning +and expert users of Isabelle. + +
+Isamode by +David Aspinall is an older and simpler Emacs interface for Isabelle. +It runs under recent versions of XEmacs. + +

Other sources of information

The Isabelle Page

+ +The Isabelle home page may be accessed both from Cambridge and Munich: + +

http://www.cl.cam.ac.uk/Research/HVG/Isabelle/ + +
http://isabelle.in.tum.de + +

+ +

Mailing list

-The electronic mailing list isabelle-users@cl.cam.ac.uk +The electronic mailing list isabelle-users@cl.cam.ac.uk provides a forum for Isabelle users to discuss problems and exchange -information. To join, send a message to -isabelle-users-request@cl.cam.ac.uk. +information. To join, send a message to isabelle-users-request@cl.cam.ac.uk.

Personal mail

@@ -130,7 +147,7 @@ Tobias Nipkow
Institut fuer Informatik
-T. U. Muenchen
+T. U. Muenchen
D-80290 Muenchen
Germany