updated for Isabelle2005;
authorwenzelm
Wed Sep 21 11:50:38 2005 +0200 (2005-09-21)
changeset 17547b0d70cf4ed18
parent 17546 07371b92d382
child 17548 4949ab06913c
updated for Isabelle2005;
COPYRIGHT
INSTALL
README.html
     1.1 --- a/COPYRIGHT	Wed Sep 21 11:50:20 2005 +0200
     1.2 +++ b/COPYRIGHT	Wed Sep 21 11:50:38 2005 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER.
     1.5  
     1.6 -Copyright (c) 2004,
     1.7 +Copyright (c) 2005,
     1.8    University of Cambridge and
     1.9    Technische Universitaet Muenchen.
    1.10  
     2.1 --- a/INSTALL	Wed Sep 21 11:50:20 2005 +0200
     2.2 +++ b/INSTALL	Wed Sep 21 11:50:38 2005 +0200
     2.3 @@ -17,7 +17,6 @@
     2.4  site installation of Isabelle on Linux/x86 works like this:
     2.5  
     2.6    tar -C /usr/local -xzf Isabelle.tar.gz
     2.7 -  tar -C /usr/local -xzf polyml_base.tar.gz
     2.8    tar -C /usr/local -xzf polyml_x86-linux.tar.gz
     2.9    tar -C /usr/local -xzf HOL_x86-linux.tar.gz
    2.10  
    2.11 @@ -27,8 +26,8 @@
    2.12  
    2.13    1) [ISABELLE_HOME]/contrib
    2.14    2) [ISABELLE_HOME]/..
    2.15 +  4) /usr/local
    2.16    3) /usr/share
    2.17 -  4) /usr/local
    2.18    5) /opt
    2.19  
    2.20  This may be changed by editing [ISABELLE_HOME]/etc/settings manually.
    2.21 @@ -49,7 +48,7 @@
    2.22  ----------------
    2.23  
    2.24  The Isabelle.tar.gz archive already contains all Isabelle sources (and
    2.25 -documentation). Precompiled object-logics are provided for
    2.26 +documentation).  Precompiled object-logics are provided for
    2.27  convenience.
    2.28  
    2.29  Assuming proper configuration of the underlying ML system
    2.30 @@ -60,7 +59,7 @@
    2.31  
    2.32  Special object-logic targets may be specified as follows:
    2.33  
    2.34 -  [ISABELLE_HOME]/build -m HOL-Complex HOL
    2.35 +  [ISABELLE_HOME]/build -m HOL-Algebra HOL
    2.36  
    2.37  
    2.38  2) User installation
     3.1 --- a/README.html	Wed Sep 21 11:50:20 2005 +0200
     3.2 +++ b/README.html	Wed Sep 21 11:50:38 2005 +0200
     3.3 @@ -21,37 +21,17 @@
     3.4  
     3.5  <h2>System requirements</h2>
     3.6  
     3.7 -<p>Isabelle requires a real Unix box with sufficient resources, say 64 MB
     3.8 -of free main memory and a decent CPU.  Speaking by today's hardware
     3.9 -standards, any moderate Linux box should give a very nice platform for
    3.10 -Isabelle.</p>
    3.11 -
    3.12 -<p>Furthermore, Isabelle needs the following software, which is not part
    3.13 -of the distribution:</p>
    3.14 -<ul>
    3.15 -    <li>A full Standard ML Compiler (e.g. Poly/ML).</li>
    3.16 -    <li>The GNU bash shell (version 1.x or 2.x).</li>
    3.17 -    <li>Perl 5.x - the Pathologically Eclectic Rubbish Lister (Perl 4.x
    3.18 -    is <em>not</em> sufficient).</li>
    3.19 -</ul>
    3.20 -
    3.21 -<p>The following ML system and platform combinations are known to work
    3.22 -very well:</p>
    3.23 +<p>Isabelle requires a regular Unix platform (e.g. GNU Linux) with the
    3.24 +following additional software:</p>
    3.25  
    3.26  <ul>
    3.27 -    <li>Poly/ML 4.x on Linux/x86, Solaris/Sparc, and PowerPC platforms.</li>
    3.28 -    <li>SML/NJ 110.x on any Unix platform (Linux, Suns, SGI etc.).</li>
    3.29 +    <li>A full Standard ML Compiler (e.g. Poly/ML 4.1.x, SML/NJ 110.x).</li>
    3.30 +    <li>The GNU bash shell (version 2.x).</li>
    3.31 +    <li>Perl (version 5.x).</li>
    3.32 +    <li>XEmacs (version 21.4.x) -- for the ProofGeneral interface.</li>
    3.33 +    <li>A complete LaTeX installation (e.g. teTeX 1.0) -- for document preparation.</li>
    3.34  </ul>
    3.35  
    3.36 -<p><a href="http://www.polyml.org/">Poly/ML</a>, previously a
    3.37 -commercial product, is back in the free world.  It is by far the best
    3.38 -compiler for running Isabelle, requiring the least memory and offering
    3.39 -the highest performance.</p>
    3.40 -
    3.41 -<p><a href="http://smlnj.sourceforge.net/">SML/NJ</a> needs more
    3.42 -store and disk space, but on the other hand supports more platforms.
    3.43 -The current official release is 110.</p>
    3.44 -
    3.45  <h2>Installation</h2>
    3.46  
    3.47  <p>Binary packages are available for Isabelle/HOL and ZF for several
    3.48 @@ -118,8 +98,8 @@
    3.49  <p>
    3.50  
    3.51  <a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a><br>
    3.52 -Institut für Informatik<br>
    3.53 -Technische Universität Mnchen<br>
    3.54 +Institut f&uuml;r Informatik<br>
    3.55 +Technische Universit&auml;t M&uuml;nchen<br>
    3.56  Boltzmannstr. 3<br>
    3.57  D-85748 Garching<br>
    3.58  Germany<br>