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ür Informatik<br>
4.105 -Technische Universität Mü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>