README.html
changeset 8809 85539b33be03
parent 8385 514df4f1df10
child 9406 d505b11ce30d
     1.1 --- a/README.html	Fri May 05 22:18:40 2000 +0200
     1.2 +++ b/README.html	Fri May 05 22:23:27 2000 +0200
     1.3 @@ -1,4 +1,3 @@
     1.4 -
     1.5  <html>
     1.6  
     1.7  <!-- $Id$ -->
     1.8 @@ -25,7 +24,7 @@
     1.9  starts at about 32-64 MB of free main memory (somewhat depending on
    1.10  your ML system), with several tens of MB disk space and a decent CPU.
    1.11  Speaking by today's hardware standards, any moderate Linux box should
    1.12 -make a nice platform for Isabelle.
    1.13 +give a very nice platform for Isabelle.
    1.14  
    1.15  <p>
    1.16  
    1.17 @@ -43,38 +42,38 @@
    1.18  The following ML system and platform combinations are known to work
    1.19  very well:
    1.20  <ul>
    1.21 -<li> Poly/ML 3.x on Linux and Suns.
    1.22 -<li> SML/NJ 110.x on any Unix platform (e.g. Linux, Suns).
    1.23 +<li> Poly/ML 3.x on Linux and Sparc/Solaris.
    1.24 +<li> SML/NJ 110.x on any Unix platform (Linux, Suns, SGI etc.).
    1.25  <li> SML/NJ 0.93 on Suns and SGIs. There seem to be several
    1.26  problems with Linux and HP-UX, though.
    1.27  </ul>
    1.28  
    1.29 -<p> <A HREF="http://www.polyml.org/">Poly/ML</A>, previously a commercial
    1.30 -product, is back in the public domain.  It is the best compiler for running
    1.31 -Isabelle, requiring the least memory and offering the fastest performance.
    1.32 +<p> <a href="http://www.polyml.org/">Poly/ML</a>, previously a
    1.33 +commercial product, is back in the free world.  It is by far the best
    1.34 +compiler for running Isabelle, requiring the least memory and offering
    1.35 +the highest performance.
    1.36  
    1.37  <p> <a
    1.38  href="http://cm.bell-labs.com/cm/cs/what/smlnj/software.html">SML/NJ</a>
    1.39 -needs lots of store and disk space, but it is free.  The current
    1.40 -official release is 110 (there is an <a
    1.41 -href="ftp://ftp.cl.cam.ac.uk/MIRRORED/smlnj/release/110/smlnj-110.0-3.i386.rpm">RPM
    1.42 -archive</a> available for Linux/x86).  We still support the old 0.93
    1.43 -release, but do not recommend it.
    1.44 +needs lots of store and disk space, but supports many more platforms.
    1.45 +The current official release is 110.  Basically, we still support the
    1.46 +old 0.93 release, but do not recommend it.
    1.47  
    1.48 -<p> MLWorks is a commercial ML programming environment developed by 
    1.49 -<a href="http://www.harlequin.com/">Harlequin</A> and was
    1.50 -unfortunately withdrawn after that company was taken over.  Isabelle on
    1.51 -MLWorks 2.0 works well.  It is about 20% faster than on SML/NJ while using
    1.52 -slightly less memory and disk space.  A few minor features (e.g. ML top-level
    1.53 -pretty printing) are not supported, though. 
    1.54 -
    1.55 +<p> MLWorks is a commercial ML programming environment developed by <a
    1.56 +href="http://www.harlequin.com/">Harlequin</a> and was unfortunately
    1.57 +withdrawn after that company was taken over.  Isabelle on MLWorks 2.0
    1.58 +works well.  It is about 20% faster than on SML/NJ while using
    1.59 +slightly less memory and disk space.  A few minor features (e.g. ML
    1.60 +top-level pretty printing) are not supported, though.
    1.61  
    1.62  
    1.63  <h2>Installation</h2>
    1.64  
    1.65 -Binary rpm packages are available for Isabelle/HOL and ZF on the
    1.66 -Linux/x86 platform.  Alternatively, the system may be built from
    1.67 -scratch as described in file <tt>INSTALL</tt> of the Isabelle sources.
    1.68 +RPM packages are available for Isabelle/HOL and ZF on the Linux/x86
    1.69 +platform.  The system may be easily built from scratch as well, taking
    1.70 +the traditional tar.gz distribution.  See file <tt>INSTALL</tt> as
    1.71 +distributed with Isabelle for more information.
    1.72 +
    1.73  Further background information may be found in the <em>Isabelle System
    1.74  Manual</em>, distributed with the sources (directory <tt>doc</tt>).
    1.75  
    1.76 @@ -82,33 +81,51 @@
    1.77  <h2>User interfaces</h2>
    1.78  
    1.79  The distribution includes only a very primitive interface based on
    1.80 -ordinary terminal sessions. Advanced interfaces are available from 
    1.81 +ordinary terminal sessions. Advanced interfaces are available from
    1.82  other sources:
    1.83  
    1.84 -<UL>
    1.85 -<LI>
    1.86 -<a href="http://www.dcs.ed.ac.uk/home/da/Isamode/">Isamode</a> by
    1.87 -David Aspinall is a more elaborate interface for Isabelle.  It runs
    1.88 -under recent versions of XEmacs and is useful to both novices and
    1.89 -experts.
    1.90 +<ul>
    1.91  
    1.92 -<LI>
    1.93 -<a href="http://www.dcs.ed.ac.uk/home/proofgen/">Proof General</a> is
    1.94 -a generic Emacs interface for proof assistants, including Isabelle
    1.95 -(both for the classic and Isar version).  Proof General is suitable
    1.96 -for use by pacifists and Emacs militants alike. Its most prominent
    1.97 -feature is script management, providing a metaphor of <em>live proof
    1.98 -script editing</em>.
    1.99 -</UL>
   1.100 +<li>
   1.101 +<a href="http://www.dcs.ed.ac.uk/home/proofgen/">Proof General</a> by
   1.102 +David Aspinall and others is a generic Emacs interface for proof
   1.103 +assistants, including Isabelle (both for the classic and Isar
   1.104 +version).  Proof General is suitable for use by pacifists and Emacs
   1.105 +militants alike. Its most prominent feature is script management,
   1.106 +providing a metaphor of <em>live proof script editing</em>.  Proof
   1.107 +General has recently gained a rather large following of both beginning
   1.108 +and expert users of Isabelle.
   1.109 +
   1.110 +<li>
   1.111 +<a href="http://www.dcs.ed.ac.uk/home/da/Isamode/">Isamode</a> by
   1.112 +David Aspinall is an older and simpler Emacs interface for Isabelle.
   1.113 +It runs under recent versions of XEmacs.
   1.114 +
   1.115 +</ul>
   1.116 +
   1.117  
   1.118  <h2>Other sources of information</h2>
   1.119  
   1.120 +<h3>The Isabelle Page</h3>
   1.121 +
   1.122 +The Isabelle home page may be accessed both from Cambridge and Munich:
   1.123 +
   1.124 +<ul>
   1.125 +
   1.126 +<li> <a
   1.127 +href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/">http://www.cl.cam.ac.uk/Research/HVG/Isabelle/</a>
   1.128 +
   1.129 +<li> <a href="http://isabelle.in.tum.de">http://isabelle.in.tum.de</a>
   1.130 +
   1.131 +</ul>
   1.132 +
   1.133 +
   1.134  <h3>Mailing list</h3>
   1.135  
   1.136 -The electronic mailing list <TT>isabelle-users@cl.cam.ac.uk</TT>
   1.137 +The electronic mailing list <tt>isabelle-users@cl.cam.ac.uk</tt>
   1.138  provides a forum for Isabelle users to discuss problems and exchange
   1.139 -information. To join, send a message to
   1.140 -<A HREF="mailto:isabelle-users-request@cl.cam.ac.uk">isabelle-users-request@cl.cam.ac.uk</A>.
   1.141 +information. To join, send a message to <a
   1.142 +href="mailto:isabelle-users-request@cl.cam.ac.uk">isabelle-users-request@cl.cam.ac.uk</a>.
   1.143  
   1.144  
   1.145  <h3>Personal mail</h3>
   1.146 @@ -130,7 +147,7 @@
   1.147  
   1.148  <a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a><br>
   1.149  Institut fuer Informatik<br>
   1.150 -T. U. Muenchen<br>	
   1.151 +T. U. Muenchen<br>
   1.152  D-80290 Muenchen<br>
   1.153  Germany<br>
   1.154  <br>