--- a/Admin/CHECKLIST Sat Oct 27 12:48:24 2007 +0200
+++ b/Admin/CHECKLIST Sat Oct 27 12:48:44 2007 +0200
@@ -3,7 +3,7 @@
- Admin/update-keywords;
-- check ANNOUNCE, README.html, INSTALL, NEWS, COPYRIGHT, CONTRIBUTORS, ~isabelle/website;
+- check ANNOUNCE, README, INSTALL, NEWS, COPYRIGHT, CONTRIBUTORS, ~isabelle/website;
- run tests with all supported ML systems;
@@ -21,7 +21,7 @@
Doc/Logics/logics.tex
- after release:
- commit new ~isabelle/website/include/documentationdist.include.html to CVS
+ commit new ~isabelle/website/include/documentationdist.include.html to website SVN
!!! commit new Admin/website/conf/distname.mak to CVS
!!! this is currently not part of CVS, so ignore this description;
!!! perhaps we will need to add it
--- a/Admin/makedist Sat Oct 27 12:48:24 2007 +0200
+++ b/Admin/makedist Sat Oct 27 12:48:44 2007 +0200
@@ -46,7 +46,7 @@
* Symlink website to Admin/website
* Check Admin/website contents.
- * Check ANNOUNCE, README.html, INSTALL, NEWS, COPYRIGHT, CONTRIBUTORS.
+ * Check ANNOUNCE, README, INSTALL, NEWS, COPYRIGHT, CONTRIBUTORS.
* Try "isatool makeall all" with Poly/ML, SML/NJ, etc.
* Tag the current repository version, e.g.:
cvs -d /usr/proj/isabelle-repository/archive rtag IsabelleXXXX isabelle
@@ -192,8 +192,7 @@
perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/index.html
perl -pi -e "s/Isabelle repository version/$DISTVERSION/" src/Pure/ROOT.ML lib/Tools/version
-perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README.html
-lynx -dump README.html >README
+perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README
( cd src; ../Admin/maketags; )
@@ -241,7 +240,7 @@
mv "$DISTNAME" "${DISTNAME}-old"
mkdir "$DISTNAME"
-mv "${DISTNAME}-old/README.html" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" \
+mv "${DISTNAME}-old/README" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" \
"${DISTNAME}-old/ANNOUNCE" "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" \
"$DISTNAME"
mkdir "$DISTNAME/doc"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/README Sat Oct 27 12:48:44 2007 +0200
@@ -0,0 +1,87 @@
+ The Isabelle System Distribution
+
+Version information
+
+ This is the internal repository version of Isabelle. See the NEWS file
+ in the distribution for details on user-relevant changes.
+
+System requirements
+
+ Isabelle requires a regular Unix platform (e.g. GNU Linux) with the
+ following additional software:
+ * A full Standard ML Compiler (e.g. Poly/ML 5.x, 4.x).
+ * The GNU bash shell (version 3.x, 2.x).
+ * Perl (version 5.x).
+ * XEmacs (version 21.4.x) -- for the ProofGeneral interface.
+ * A complete LaTeX installation -- for document preparation.
+
+Installation
+
+ Binary packages are available for Isabelle/HOL and ZF for several
+ platforms from the Isabelle web page. The system may be easily built
+ from scratch as well, taking the traditional tar.gz source
+ 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).
+
+User interface
+
+ The canonical Isabelle user interface is [1]Proof General by David
+ Aspinall and others. It is a generic (X)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.
+
+ Proof General is distributed together with the XEmacs [2]X-Symbol
+ package, which provides a nice way to get proper mathematical symbols
+ displayed on screen.
+
+Other sources of information
+
+ The Isabelle Page
+
+ The Isabelle home page may be accessed both from Cambridge and Munich:
+ * [3]http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
+ * [4]http://isabelle.in.tum.de
+
+ Mailing list
+
+ 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 [5]isabelle-users-request@cl.cam.ac.uk.
+
+ Personal mail
+
+ [6]Lawrence C Paulson
+ Computer Laboratory
+ University of Cambridge
+ JJ Thomson Avenue
+ Cambridge CB3 0FD
+ England
+ E-mail: [7]lcp@cl.cam.ac.uk
+ Phone: +44-223-763500
+ Fax: +44-223-334748
+
+ or
+
+ [8]Tobias Nipkow
+ Institut für Informatik
+ Technische Universität München
+ Boltzmannstr. 3
+ D-85748 Garching
+ Germany
+ E-mail: [9]nipkow@in.tum.de
+ Phone: +49-89-289-17302
+ Fax: +49-89-289-17307
+ _________________________________________________________________
+
+ Please report any problems you encounter. While we shall try to be
+ helpful, we can accept no responsibility for the deficiencies of
+ Isabelle and their consequences.
+ _________________________________________________________________
+
--- a/README.html Sat Oct 27 12:48:24 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,121 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-
-<!-- $Id$ -->
-
-<html>
-
-<head>
- <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
- <title>The Isabelle System Distribution</title>
-</head>
-
-<body>
-
-<h1>The Isabelle System Distribution</h1>
-
-<h2>Version information</h2>
-
-<p>This is the internal repository version of Isabelle. See the
-<tt>NEWS</tt> file in the distribution for details on user-relevant
-changes.</p>
-
-<h2>System requirements</h2>
-
-<p>Isabelle requires a regular Unix platform (e.g. GNU Linux) with the
-following additional software:</p>
-
-<ul>
- <li>A full Standard ML Compiler (e.g. Poly/ML 5.x, 4.x).</li>
- <li>The GNU bash shell (version 3.x, 2.x).</li>
- <li>Perl (version 5.x).</li>
- <li>XEmacs (version 21.4.x) -- for the ProofGeneral interface.</li>
- <li>A complete LaTeX installation -- for document preparation.</li>
-</ul>
-
-<h2>Installation</h2>
-
-<p>Binary packages are available for Isabelle/HOL and ZF for several
-platforms from the Isabelle web page. The system may be easily built
-from scratch as well, taking the traditional tar.gz source
-distribution. See file <tt>INSTALL</tt> as distributed with Isabelle
-for more information.</p>
-
-<p>Further background information may be found in the <em>Isabelle System
-Manual</em>, distributed with the sources (directory <tt>doc</tt>).</p>
-
-<h2>User interface</h2>
-
-<p>The canonical Isabelle user interface is <a
-href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a> by David Aspinall
-and others. It is a generic (X)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 <em>live proof script editing</em>. Proof General has
-recently gained a rather large following of both beginning and expert
-users of Isabelle.</p>
-
-<p>Proof General is distributed together with the XEmacs
-<a href="http://x-symbol.sourceforge.net">
-X-Symbol package</a>, which provides a nice way to get proper
-mathematical symbols displayed on screen.</p>
-
-<h2>Other sources of information</h2>
-
-<h3>The Isabelle Page</h3>
-
-<p>The Isabelle home page may be accessed both from Cambridge and Munich:</p>
-
-<ul>
- <li><a href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/">http://www.cl.cam.ac.uk/Research/HVG/Isabelle/</a></li>
- <li><a href="http://isabelle.in.tum.de">http://isabelle.in.tum.de</a></li>
-</ul>
-
-
-<h3>Mailing list</h3>
-
-<p>The electronic mailing list <tt>isabelle-users@cl.cam.ac.uk</tt>
-provides a forum for Isabelle users to discuss problems and exchange
-information. To join, send a message to <a
-href="mailto:isabelle-users-request@cl.cam.ac.uk">isabelle-users-request@cl.cam.ac.uk</a>.</p>
-
-
-<h3>Personal mail</h3>
-
-<a href="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C Paulson</a><br>
-Computer Laboratory<br>
-University of Cambridge<br>
-JJ Thomson Avenue<br>
-Cambridge CB3 0FD<br>
-England<br>
-<br>
-E-mail: <a href="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</a><br>
-Phone: +44-223-763500<br>
-Fax: +44-223-334748<br>
-
-<p>
-or
-<p>
-
-<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a><br>
-Institut für Informatik<br>
-Technische Universität München<br>
-Boltzmannstr. 3<br>
-D-85748 Garching<br>
-Germany<br>
-<br>
-E-mail: <a href="mailto:nipkow@in.tum.de">nipkow@in.tum.de</a><br>
-Phone: +49-89-289-17302<br>
-Fax: +49-89-289-17307<br>
-<p>
-
-<hr>
-
-Please report any problems you encounter. While we shall try to be
-helpful, we can accept no responsibility for the deficiencies of
-Isabelle and their consequences.
-
-<hr>
-
-</body>
-</html>