| author | berghofe |
| Mon, 17 Oct 2005 17:42:24 +0200 | |
| changeset 17872 | f08fc98a164a |
| parent 17547 | b0d70cf4ed18 |
| child 25126 | 705f54aeba7c |
| permissions | -rw-r--r-- |
| webertj@15278 | 1 |
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> |
| webertj@15278 | 2 |
|
| webertj@15582 | 3 |
<!-- $Id$ --> |
| webertj@15582 | 4 |
|
| wenzelm@3259 | 5 |
<html> |
| wenzelm@3259 | 6 |
|
| wenzelm@3259 | 7 |
<head> |
| webertj@15278 | 8 |
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"> |
| webertj@15278 | 9 |
<title>The Isabelle System Distribution</title> |
| wenzelm@3259 | 10 |
</head> |
| wenzelm@3259 | 11 |
|
| wenzelm@3259 | 12 |
<body> |
| wenzelm@3259 | 13 |
|
| wenzelm@3259 | 14 |
<h1>The Isabelle System Distribution</h1> |
| wenzelm@3259 | 15 |
|
| wenzelm@3259 | 16 |
<h2>Version information</h2> |
| wenzelm@3259 | 17 |
|
| haftmann@16327 | 18 |
<p>This is the internal repository version of Isabelle. See the |
| wenzelm@11575 | 19 |
<tt>NEWS</tt> file in the distribution for details on user-relevant |
| haftmann@16327 | 20 |
changes.</p> |
| wenzelm@3259 | 21 |
|
| wenzelm@3259 | 22 |
<h2>System requirements</h2> |
| wenzelm@3259 | 23 |
|
| wenzelm@17547 | 24 |
<p>Isabelle requires a regular Unix platform (e.g. GNU Linux) with the |
| wenzelm@17547 | 25 |
following additional software:</p> |
| wenzelm@3259 | 26 |
|
| wenzelm@3259 | 27 |
<ul> |
| wenzelm@17547 | 28 |
<li>A full Standard ML Compiler (e.g. Poly/ML 4.1.x, SML/NJ 110.x).</li> |
| wenzelm@17547 | 29 |
<li>The GNU bash shell (version 2.x).</li> |
| wenzelm@17547 | 30 |
<li>Perl (version 5.x).</li> |
| wenzelm@17547 | 31 |
<li>XEmacs (version 21.4.x) -- for the ProofGeneral interface.</li> |
| wenzelm@17547 | 32 |
<li>A complete LaTeX installation (e.g. teTeX 1.0) -- for document preparation.</li> |
| wenzelm@3259 | 33 |
</ul> |
| wenzelm@3259 | 34 |
|
| wenzelm@3259 | 35 |
<h2>Installation</h2> |
| wenzelm@3259 | 36 |
|
| haftmann@16327 | 37 |
<p>Binary packages are available for Isabelle/HOL and ZF for several |
| kleing@14007 | 38 |
platforms from the Isabelle web page. The system may be easily built |
| kleing@14007 | 39 |
from scratch as well, taking the traditional tar.gz source |
| kleing@14007 | 40 |
distribution. See file <tt>INSTALL</tt> as distributed with Isabelle |
| haftmann@16327 | 41 |
for more information.</p> |
| wenzelm@8809 | 42 |
|
| haftmann@16327 | 43 |
<p>Further background information may be found in the <em>Isabelle System |
| haftmann@16327 | 44 |
Manual</em>, distributed with the sources (directory <tt>doc</tt>).</p> |
| wenzelm@3259 | 45 |
|
| wenzelm@9927 | 46 |
<h2>User interface</h2> |
| wenzelm@3306 | 47 |
|
| haftmann@16327 | 48 |
<p>The canonical Isabelle user interface is <a |
| kleing@14298 | 49 |
href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a> by David Aspinall |
| wenzelm@10079 | 50 |
and others. It is a generic (X)Emacs interface for proof assistants, |
| wenzelm@10079 | 51 |
including Isabelle (both for the classic and Isar version). Proof |
| wenzelm@10079 | 52 |
General is suitable for use by pacifists and Emacs militants |
| wenzelm@10079 | 53 |
alike. Its most prominent feature is script management, providing a |
| wenzelm@10079 | 54 |
metaphor of <em>live proof script editing</em>. Proof General has |
| wenzelm@10079 | 55 |
recently gained a rather large following of both beginning and expert |
| haftmann@16327 | 56 |
users of Isabelle.</p> |
| wenzelm@8809 | 57 |
|
| haftmann@16327 | 58 |
<p>Proof General is distributed together with the XEmacs |
| wenzelm@13141 | 59 |
<a href="http://x-symbol.sourceforge.net"> |
| wenzelm@9927 | 60 |
X-Symbol package</a>, which provides a nice way to get proper |
| haftmann@16327 | 61 |
mathematical symbols displayed on screen.</p> |
| wenzelm@3306 | 62 |
|
| wenzelm@3259 | 63 |
<h2>Other sources of information</h2> |
| wenzelm@3259 | 64 |
|
| wenzelm@8809 | 65 |
<h3>The Isabelle Page</h3> |
| wenzelm@8809 | 66 |
|
| haftmann@16327 | 67 |
<p>The Isabelle home page may be accessed both from Cambridge and Munich:</p> |
| wenzelm@8809 | 68 |
|
| wenzelm@8809 | 69 |
<ul> |
| haftmann@16327 | 70 |
<li><a href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/">http://www.cl.cam.ac.uk/Research/HVG/Isabelle/</a></li> |
| haftmann@16327 | 71 |
<li><a href="http://isabelle.in.tum.de">http://isabelle.in.tum.de</a></li> |
| wenzelm@8809 | 72 |
</ul> |
| wenzelm@8809 | 73 |
|
| wenzelm@8809 | 74 |
|
| wenzelm@3259 | 75 |
<h3>Mailing list</h3> |
| wenzelm@3259 | 76 |
|
| haftmann@16327 | 77 |
<p>The electronic mailing list <tt>isabelle-users@cl.cam.ac.uk</tt> |
| wenzelm@3259 | 78 |
provides a forum for Isabelle users to discuss problems and exchange |
| wenzelm@8809 | 79 |
information. To join, send a message to <a |
| haftmann@16327 | 80 |
href="mailto:isabelle-users-request@cl.cam.ac.uk">isabelle-users-request@cl.cam.ac.uk</a>.</p> |
| wenzelm@3259 | 81 |
|
| wenzelm@3259 | 82 |
|
| wenzelm@3259 | 83 |
<h3>Personal mail</h3> |
| wenzelm@3259 | 84 |
|
| wenzelm@3259 | 85 |
<a href="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C Paulson</a><br> |
| wenzelm@3259 | 86 |
Computer Laboratory<br> |
| wenzelm@3259 | 87 |
University of Cambridge<br> |
| paulson@14628 | 88 |
JJ Thomson Avenue<br> |
| paulson@14628 | 89 |
Cambridge CB3 0FD<br> |
| wenzelm@3259 | 90 |
England<br> |
| wenzelm@3259 | 91 |
<br> |
| haftmann@16327 | 92 |
E-mail: <a href="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</a><br> |
| paulson@14629 | 93 |
Phone: +44-223-763500<br> |
| wenzelm@3259 | 94 |
Fax: +44-223-334748<br> |
| wenzelm@3259 | 95 |
|
| wenzelm@3259 | 96 |
<p> |
| wenzelm@3259 | 97 |
or |
| wenzelm@3259 | 98 |
<p> |
| wenzelm@3259 | 99 |
|
| wenzelm@5401 | 100 |
<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a><br> |
| wenzelm@17547 | 101 |
Institut für Informatik<br> |
| wenzelm@17547 | 102 |
Technische Universität München<br> |
| kleing@14622 | 103 |
Boltzmannstr. 3<br> |
| kleing@14622 | 104 |
D-85748 Garching<br> |
| wenzelm@3259 | 105 |
Germany<br> |
| wenzelm@3259 | 106 |
<br> |
| haftmann@16327 | 107 |
E-mail: <a href="mailto:nipkow@in.tum.de">nipkow@in.tum.de</a><br> |
| kleing@14622 | 108 |
Phone: +49-89-289-17302<br> |
| kleing@14622 | 109 |
Fax: +49-89-289-17307<br> |
| wenzelm@3259 | 110 |
<p> |
| wenzelm@3259 | 111 |
|
| wenzelm@3259 | 112 |
<hr> |
| wenzelm@3259 | 113 |
|
| wenzelm@3259 | 114 |
Please report any problems you encounter. While we shall try to be |
| wenzelm@5665 | 115 |
helpful, we can accept no responsibility for the deficiencies of |
| wenzelm@3259 | 116 |
Isabelle and their consequences. |
| wenzelm@3259 | 117 |
|
| wenzelm@3259 | 118 |
<hr> |
| wenzelm@3259 | 119 |
|
| wenzelm@3259 | 120 |
</body> |
| wenzelm@3259 | 121 |
</html> |