--- 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>