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