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