ASCIIfied README
authorhaftmann
Sat Oct 27 12:48:44 2007 +0200 (2007-10-27)
changeset 2521491730b492a45
parent 25213 48a1e80f5cdb
child 25215 f53dc3c413f5
ASCIIfied README
Admin/CHECKLIST
Admin/makedist
README
README.html
     1.1 --- a/Admin/CHECKLIST	Sat Oct 27 12:48:24 2007 +0200
     1.2 +++ b/Admin/CHECKLIST	Sat Oct 27 12:48:44 2007 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4  
     1.5  - Admin/update-keywords;
     1.6  
     1.7 -- check ANNOUNCE, README.html, INSTALL, NEWS, COPYRIGHT, CONTRIBUTORS, ~isabelle/website;
     1.8 +- check ANNOUNCE, README, INSTALL, NEWS, COPYRIGHT, CONTRIBUTORS, ~isabelle/website;
     1.9  
    1.10  - run tests with all supported ML systems;
    1.11  
    1.12 @@ -21,7 +21,7 @@
    1.13      Doc/Logics/logics.tex
    1.14  
    1.15  - after release: 
    1.16 -    commit new ~isabelle/website/include/documentationdist.include.html to CVS
    1.17 +    commit new ~isabelle/website/include/documentationdist.include.html to website SVN
    1.18      !!! commit new Admin/website/conf/distname.mak to CVS
    1.19      !!! this is currently not part of CVS, so ignore this description;
    1.20      !!! perhaps we will need to add it
     2.1 --- a/Admin/makedist	Sat Oct 27 12:48:24 2007 +0200
     2.2 +++ b/Admin/makedist	Sat Oct 27 12:48:44 2007 +0200
     2.3 @@ -46,7 +46,7 @@
     2.4  
     2.5      * Symlink website to Admin/website
     2.6      * Check Admin/website contents.
     2.7 -    * Check ANNOUNCE, README.html, INSTALL, NEWS, COPYRIGHT, CONTRIBUTORS.
     2.8 +    * Check ANNOUNCE, README, INSTALL, NEWS, COPYRIGHT, CONTRIBUTORS.
     2.9      * Try "isatool makeall all" with Poly/ML, SML/NJ, etc.
    2.10      * Tag the current repository version, e.g.:
    2.11          cvs -d /usr/proj/isabelle-repository/archive rtag IsabelleXXXX isabelle
    2.12 @@ -192,8 +192,7 @@
    2.13  
    2.14  perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/index.html
    2.15  perl -pi -e "s/Isabelle repository version/$DISTVERSION/" src/Pure/ROOT.ML lib/Tools/version
    2.16 -perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README.html
    2.17 -lynx -dump README.html >README
    2.18 +perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README
    2.19  
    2.20  ( cd src; ../Admin/maketags; )
    2.21  
    2.22 @@ -241,7 +240,7 @@
    2.23  mv "$DISTNAME" "${DISTNAME}-old"
    2.24  mkdir "$DISTNAME"
    2.25  
    2.26 -mv "${DISTNAME}-old/README.html" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" \
    2.27 +mv "${DISTNAME}-old/README" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" \
    2.28    "${DISTNAME}-old/ANNOUNCE" "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" \
    2.29    "$DISTNAME"
    2.30  mkdir "$DISTNAME/doc"
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/README	Sat Oct 27 12:48:44 2007 +0200
     3.3 @@ -0,0 +1,87 @@
     3.4 +                       The Isabelle System Distribution
     3.5 +
     3.6 +Version information
     3.7 +
     3.8 +   This is the internal repository version of Isabelle. See the NEWS file
     3.9 +   in the distribution for details on user-relevant changes.
    3.10 +
    3.11 +System requirements
    3.12 +
    3.13 +   Isabelle requires a regular Unix platform (e.g. GNU Linux) with the
    3.14 +   following additional software:
    3.15 +     * A full Standard ML Compiler (e.g. Poly/ML 5.x, 4.x).
    3.16 +     * The GNU bash shell (version 3.x, 2.x).
    3.17 +     * Perl (version 5.x).
    3.18 +     * XEmacs (version 21.4.x) -- for the ProofGeneral interface.
    3.19 +     * A complete LaTeX installation -- for document preparation.
    3.20 +
    3.21 +Installation
    3.22 +
    3.23 +   Binary packages are available for Isabelle/HOL and ZF for several
    3.24 +   platforms from the Isabelle web page. The system may be easily built
    3.25 +   from scratch as well, taking the traditional tar.gz source
    3.26 +   distribution. See file INSTALL as distributed with Isabelle for more
    3.27 +   information.
    3.28 +
    3.29 +   Further background information may be found in the Isabelle System
    3.30 +   Manual, distributed with the sources (directory doc).
    3.31 +
    3.32 +User interface
    3.33 +
    3.34 +   The canonical Isabelle user interface is [1]Proof General by David
    3.35 +   Aspinall and others. It is a generic (X)Emacs interface for proof
    3.36 +   assistants, including Isabelle (both for the classic and Isar
    3.37 +   version). Proof General is suitable for use by pacifists and Emacs
    3.38 +   militants alike. Its most prominent feature is script management,
    3.39 +   providing a metaphor of live proof script editing. Proof General has
    3.40 +   recently gained a rather large following of both beginning and expert
    3.41 +   users of Isabelle.
    3.42 +
    3.43 +   Proof General is distributed together with the XEmacs [2]X-Symbol
    3.44 +   package, which provides a nice way to get proper mathematical symbols
    3.45 +   displayed on screen.
    3.46 +
    3.47 +Other sources of information
    3.48 +
    3.49 +  The Isabelle Page
    3.50 +
    3.51 +   The Isabelle home page may be accessed both from Cambridge and Munich:
    3.52 +     * [3]http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
    3.53 +     * [4]http://isabelle.in.tum.de
    3.54 +
    3.55 +  Mailing list
    3.56 +
    3.57 +   The electronic mailing list isabelle-users@cl.cam.ac.uk provides a
    3.58 +   forum for Isabelle users to discuss problems and exchange information.
    3.59 +   To join, send a message to [5]isabelle-users-request@cl.cam.ac.uk.
    3.60 +
    3.61 +  Personal mail
    3.62 +
    3.63 +   [6]Lawrence C Paulson
    3.64 +   Computer Laboratory
    3.65 +   University of Cambridge
    3.66 +   JJ Thomson Avenue
    3.67 +   Cambridge CB3 0FD
    3.68 +   England
    3.69 +   E-mail: [7]lcp@cl.cam.ac.uk
    3.70 +   Phone: +44-223-763500
    3.71 +   Fax: +44-223-334748
    3.72 +
    3.73 +   or
    3.74 +
    3.75 +   [8]Tobias Nipkow
    3.76 +   Institut für Informatik
    3.77 +   Technische Universität München
    3.78 +   Boltzmannstr. 3
    3.79 +   D-85748 Garching
    3.80 +   Germany
    3.81 +   E-mail: [9]nipkow@in.tum.de
    3.82 +   Phone: +49-89-289-17302
    3.83 +   Fax: +49-89-289-17307
    3.84 +     _________________________________________________________________
    3.85 +
    3.86 +   Please report any problems you encounter. While we shall try to be
    3.87 +   helpful, we can accept no responsibility for the deficiencies of
    3.88 +   Isabelle and their consequences.
    3.89 +     _________________________________________________________________
    3.90 +
     4.1 --- a/README.html	Sat Oct 27 12:48:24 2007 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,121 +0,0 @@
     4.4 -<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     4.5 -
     4.6 -<!-- $Id$ -->
     4.7 -
     4.8 -<html>
     4.9 -
    4.10 -<head>
    4.11 -  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
    4.12 -  <title>The Isabelle System Distribution</title>
    4.13 -</head>
    4.14 -
    4.15 -<body>
    4.16 -
    4.17 -<h1>The Isabelle System Distribution</h1>
    4.18 -
    4.19 -<h2>Version information</h2>
    4.20 -
    4.21 -<p>This is the internal repository version of Isabelle. See the
    4.22 -<tt>NEWS</tt> file in the distribution for details on user-relevant
    4.23 -changes.</p>
    4.24 -
    4.25 -<h2>System requirements</h2>
    4.26 -
    4.27 -<p>Isabelle requires a regular Unix platform (e.g. GNU Linux) with the
    4.28 -following additional software:</p>
    4.29 -
    4.30 -<ul>
    4.31 -    <li>A full Standard ML Compiler (e.g. Poly/ML 5.x, 4.x).</li>
    4.32 -    <li>The GNU bash shell (version 3.x, 2.x).</li>
    4.33 -    <li>Perl (version 5.x).</li>
    4.34 -    <li>XEmacs (version 21.4.x) -- for the ProofGeneral interface.</li>
    4.35 -    <li>A complete LaTeX installation -- for document preparation.</li>
    4.36 -</ul>
    4.37 -
    4.38 -<h2>Installation</h2>
    4.39 -
    4.40 -<p>Binary packages are available for Isabelle/HOL and ZF for several
    4.41 -platforms from the Isabelle web page.  The system may be easily built
    4.42 -from scratch as well, taking the traditional tar.gz source
    4.43 -distribution.  See file <tt>INSTALL</tt> as distributed with Isabelle
    4.44 -for more information.</p>
    4.45 -
    4.46 -<p>Further background information may be found in the <em>Isabelle System
    4.47 -Manual</em>, distributed with the sources (directory <tt>doc</tt>).</p>
    4.48 -
    4.49 -<h2>User interface</h2>
    4.50 -
    4.51 -<p>The canonical Isabelle user interface is <a
    4.52 -href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a> by David Aspinall
    4.53 -and others.  It is a generic (X)Emacs interface for proof assistants,
    4.54 -including Isabelle (both for the classic and Isar version).  Proof
    4.55 -General is suitable for use by pacifists and Emacs militants
    4.56 -alike. Its most prominent feature is script management, providing a
    4.57 -metaphor of <em>live proof script editing</em>.  Proof General has
    4.58 -recently gained a rather large following of both beginning and expert
    4.59 -users of Isabelle.</p>
    4.60 -
    4.61 -<p>Proof General is distributed together with the XEmacs
    4.62 -<a href="http://x-symbol.sourceforge.net">
    4.63 -X-Symbol package</a>, which provides a nice way to get proper
    4.64 -mathematical symbols displayed on screen.</p>
    4.65 -
    4.66 -<h2>Other sources of information</h2>
    4.67 -
    4.68 -<h3>The Isabelle Page</h3>
    4.69 -
    4.70 -<p>The Isabelle home page may be accessed both from Cambridge and Munich:</p>
    4.71 -
    4.72 -<ul>
    4.73 -    <li><a href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/">http://www.cl.cam.ac.uk/Research/HVG/Isabelle/</a></li>
    4.74 -    <li><a href="http://isabelle.in.tum.de">http://isabelle.in.tum.de</a></li>
    4.75 -</ul>
    4.76 -
    4.77 -
    4.78 -<h3>Mailing list</h3>
    4.79 -
    4.80 -<p>The electronic mailing list <tt>isabelle-users@cl.cam.ac.uk</tt>
    4.81 -provides a forum for Isabelle users to discuss problems and exchange
    4.82 -information. To join, send a message to <a
    4.83 -href="mailto:isabelle-users-request@cl.cam.ac.uk">isabelle-users-request@cl.cam.ac.uk</a>.</p>
    4.84 -
    4.85 -
    4.86 -<h3>Personal mail</h3>
    4.87 -
    4.88 -<a href="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C Paulson</a><br>
    4.89 -Computer Laboratory<br>
    4.90 -University of Cambridge<br>
    4.91 -JJ Thomson Avenue<br>
    4.92 -Cambridge CB3 0FD<br>
    4.93 -England<br>
    4.94 -<br>
    4.95 -E-mail: <a href="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</a><br>
    4.96 -Phone: +44-223-763500<br>
    4.97 -Fax:   +44-223-334748<br>
    4.98 -
    4.99 -<p>
   4.100 -or
   4.101 -<p>
   4.102 -
   4.103 -<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a><br>
   4.104 -Institut f&uuml;r Informatik<br>
   4.105 -Technische Universit&auml;t M&uuml;nchen<br>
   4.106 -Boltzmannstr. 3<br>
   4.107 -D-85748 Garching<br>
   4.108 -Germany<br>
   4.109 -<br>
   4.110 -E-mail: <a href="mailto:nipkow@in.tum.de">nipkow@in.tum.de</a><br>
   4.111 -Phone: +49-89-289-17302<br>
   4.112 -Fax:   +49-89-289-17307<br>
   4.113 -<p>
   4.114 -
   4.115 -<hr>
   4.116 -
   4.117 -Please report any problems you encounter.  While we shall try to be
   4.118 -helpful, we can accept no responsibility for the deficiencies of
   4.119 -Isabelle and their consequences.
   4.120 -
   4.121 -<hr>
   4.122 -
   4.123 -</body>
   4.124 -</html>