author | wenzelm |
Tue, 26 Aug 2008 12:17:58 +0200 | |
changeset 28002 | 95bd956c476c |
parent 27646 | d010fc1d3c46 |
child 30852 | 59a422908e29 |
permissions | -rw-r--r-- |
haftmann@25214 | 1 |
The Isabelle System Distribution |
haftmann@25214 | 2 |
|
haftmann@25214 | 3 |
Version information |
haftmann@25214 | 4 |
|
wenzelm@27646 | 5 |
This is the internal repository version of Isabelle. |
wenzelm@27646 | 6 |
|
wenzelm@27646 | 7 |
See the NEWS file in the distribution for details on user-relevant |
wenzelm@27646 | 8 |
changes. |
haftmann@25214 | 9 |
|
haftmann@25214 | 10 |
System requirements |
haftmann@25214 | 11 |
|
haftmann@25214 | 12 |
Isabelle requires a regular Unix platform (e.g. GNU Linux) with the |
haftmann@25214 | 13 |
following additional software: |
wenzelm@27006 | 14 |
* A full Standard ML Compiler (works best with Poly/ML 5.x). |
wenzelm@27006 | 15 |
* The GNU bash shell (version 3.x or 2.x). |
haftmann@25214 | 16 |
* Perl (version 5.x). |
wenzelm@27006 | 17 |
* GNU Emacs (version 21, 22) or XEmacs (version 21.4.x) |
wenzelm@25447 | 18 |
-- for the Proof General interface. |
haftmann@25214 | 19 |
* A complete LaTeX installation -- for document preparation. |
haftmann@25214 | 20 |
|
haftmann@25214 | 21 |
Installation |
haftmann@25214 | 22 |
|
haftmann@25214 | 23 |
Binary packages are available for Isabelle/HOL and ZF for several |
wenzelm@25447 | 24 |
platforms from the Isabelle web page. The system may be easily |
wenzelm@25447 | 25 |
built from scratch as well, taking the traditional tar.gz source |
wenzelm@25447 | 26 |
distribution. See file INSTALL as distributed with Isabelle for |
wenzelm@25447 | 27 |
more information. |
haftmann@25214 | 28 |
|
haftmann@25214 | 29 |
Further background information may be found in the Isabelle System |
haftmann@25214 | 30 |
Manual, distributed with the sources (directory doc). |
haftmann@25214 | 31 |
|
haftmann@25214 | 32 |
User interface |
haftmann@25214 | 33 |
|
wenzelm@25415 | 34 |
The canonical Isabelle user interface is Proof General by David |
haftmann@25214 | 35 |
Aspinall and others. It is a generic (X)Emacs interface for proof |
wenzelm@25447 | 36 |
assistants, including Isabelle. Proof General is suitable for use |
wenzelm@25447 | 37 |
by pacifists and Emacs militants alike. Its most prominent feature |
wenzelm@25447 | 38 |
is script management, providing a metaphor of live proof script |
wenzelm@25447 | 39 |
editing. |
haftmann@25214 | 40 |
|
wenzelm@25415 | 41 |
Proof General is distributed together with the XEmacs X-Symbol |
wenzelm@25447 | 42 |
package, which provides a reasonable way to get proper mathematical |
wenzelm@25447 | 43 |
symbols displayed on screen. |
haftmann@25214 | 44 |
|
haftmann@25214 | 45 |
Other sources of information |
haftmann@25214 | 46 |
|
haftmann@25214 | 47 |
The Isabelle Page |
haftmann@25214 | 48 |
|
haftmann@25214 | 49 |
The Isabelle home page may be accessed both from Cambridge and Munich: |
haftmann@27085 | 50 |
* http://www.cl.cam.ac.uk/research/hvg/Isabelle/ |
wenzelm@25415 | 51 |
* http://isabelle.in.tum.de |
haftmann@25214 | 52 |
|
haftmann@25214 | 53 |
Mailing list |
haftmann@25214 | 54 |
|
haftmann@25214 | 55 |
The electronic mailing list isabelle-users@cl.cam.ac.uk provides a |
wenzelm@25447 | 56 |
forum for Isabelle users to discuss problems and exchange |
wenzelm@25447 | 57 |
information. To join, send a message to |
wenzelm@25447 | 58 |
isabelle-users-request@cl.cam.ac.uk. |
haftmann@25214 | 59 |
|
haftmann@25214 | 60 |
Personal mail |
haftmann@25214 | 61 |
|
wenzelm@25415 | 62 |
Lawrence C Paulson |
haftmann@25214 | 63 |
Computer Laboratory |
haftmann@25214 | 64 |
University of Cambridge |
haftmann@25214 | 65 |
JJ Thomson Avenue |
haftmann@25214 | 66 |
Cambridge CB3 0FD |
haftmann@25214 | 67 |
England |
wenzelm@25415 | 68 |
E-mail: lcp@cl.cam.ac.uk |
haftmann@25214 | 69 |
Phone: +44-223-763500 |
haftmann@25214 | 70 |
Fax: +44-223-334748 |
haftmann@25214 | 71 |
|
haftmann@25214 | 72 |
or |
haftmann@25214 | 73 |
|
wenzelm@25415 | 74 |
Tobias Nipkow |
wenzelm@25415 | 75 |
Institut fuer Informatik |
wenzelm@25415 | 76 |
Technische Universitaet Muenchen |
haftmann@25214 | 77 |
Boltzmannstr. 3 |
haftmann@25214 | 78 |
D-85748 Garching |
haftmann@25214 | 79 |
Germany |
wenzelm@25415 | 80 |
E-mail: nipkow@in.tum.de |
haftmann@25214 | 81 |
Phone: +49-89-289-17302 |
haftmann@25214 | 82 |
Fax: +49-89-289-17307 |
haftmann@25214 | 83 |
_________________________________________________________________ |
haftmann@25214 | 84 |
|
haftmann@25214 | 85 |
Please report any problems you encounter. While we shall try to be |
haftmann@25214 | 86 |
helpful, we can accept no responsibility for the deficiencies of |
haftmann@25214 | 87 |
Isabelle and their consequences. |
haftmann@25214 | 88 |
_________________________________________________________________ |