haftmann@25214
|
1 |
The Isabelle System Distribution
|
haftmann@25214
|
2 |
|
haftmann@25214
|
3 |
Version information
|
haftmann@25214
|
4 |
|
wenzelm@32361
|
5 |
This is some unidentified 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 |
|
wenzelm@37159
|
12 |
Isabelle requires a regular Unix-style platform (e.g. Linux,
|
wenzelm@37159
|
13 |
Windows with Cygwin, Mac OS) and depends on the following main
|
wenzelm@37159
|
14 |
add-on tools:
|
wenzelm@33842
|
15 |
|
wenzelm@38788
|
16 |
* The Poly/ML compiler and runtime system (version 5.2.1 or later).
|
wenzelm@27006
|
17 |
* The GNU bash shell (version 3.x or 2.x).
|
haftmann@25214
|
18 |
* Perl (version 5.x).
|
wenzelm@41775
|
19 |
* GNU Emacs (version 23) -- for the Proof General 4.x interface.
|
wenzelm@41844
|
20 |
* Java 1.6.x from Oracle/Sun or Apple -- for Scala and jEdit.
|
haftmann@25214
|
21 |
* A complete LaTeX installation -- for document preparation.
|
haftmann@25214
|
22 |
|
haftmann@25214
|
23 |
Installation
|
haftmann@25214
|
24 |
|
wenzelm@37469
|
25 |
Completely integrated bundles including the full Isabelle sources,
|
wenzelm@37469
|
26 |
documentation, add-on tools and precompiled logic images for
|
wenzelm@37469
|
27 |
several platforms are available from the Isabelle web page.
|
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@36865
|
34 |
The classic Isabelle user interface is Proof General by David
|
wenzelm@41844
|
35 |
Aspinall and others. It is a generic Emacs interface for proof
|
wenzelm@37159
|
36 |
assistants, including Isabelle. Its most prominent feature is
|
wenzelm@37159
|
37 |
script management, providing a metaphor of stepwise proof script
|
wenzelm@41844
|
38 |
editing.
|
wenzelm@41844
|
39 |
|
wenzelm@41844
|
40 |
Isabelle/jEdit is an experimental Prover IDE based on advanced
|
wenzelm@41844
|
41 |
technology of Isabelle/Scala. It provides a metaphor of continuous
|
wenzelm@41844
|
42 |
proof checking of a versioned collection of theory sources, with
|
wenzelm@41844
|
43 |
instantaneous feedback in real-time.
|
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 |
_________________________________________________________________
|