| author | wenzelm | 
| Sat, 01 Sep 2012 19:46:21 +0200 | |
| changeset 49063 | f93443defa6c | 
| parent 47805 | 5d283dca6104 | 
| child 50572 | b33912e68b84 | 
| 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  | 
|
| 
47795
 
ccb10fe4b955
some updates on classic README, reduce the impression that there is much to install manually;
 
wenzelm 
parents: 
47745 
diff
changeset
 | 
10  | 
Installation  | 
| 33842 | 11  | 
|
| 47805 | 12  | 
Isabelle works on the three main platform families: Linux, Mac OS  | 
13  | 
X, and Windows (via Cygwin).  | 
|
| 25214 | 14  | 
|
| 37368 | 15  | 
Completely integrated bundles including the full Isabelle sources,  | 
16  | 
documentation, add-on tools and precompiled logic images for  | 
|
17  | 
several platforms are available from the Isabelle web page.  | 
|
| 25214 | 18  | 
|
| 
47795
 
ccb10fe4b955
some updates on classic README, reduce the impression that there is much to install manually;
 
wenzelm 
parents: 
47745 
diff
changeset
 | 
19  | 
Some background information may be found in the Isabelle System  | 
| 25214 | 20  | 
Manual, distributed with the sources (directory doc).  | 
21  | 
||
| 
47795
 
ccb10fe4b955
some updates on classic README, reduce the impression that there is much to install manually;
 
wenzelm 
parents: 
47745 
diff
changeset
 | 
22  | 
User interfaces  | 
| 25214 | 23  | 
|
| 44801 | 24  | 
Isabelle/jEdit is an emerging Prover IDE based on advanced  | 
25  | 
technology of Isabelle/Scala. It provides a metaphor of continuous  | 
|
26  | 
proof checking of a versioned collection of theory sources, with  | 
|
27  | 
instantaneous feedback in real-time and rich semantic markup  | 
|
28  | 
associated with the formal text.  | 
|
29  | 
||
| 36858 | 30  | 
The classic Isabelle user interface is Proof General by David  | 
| 41596 | 31  | 
Aspinall and others. It is a generic Emacs interface for proof  | 
| 47805 | 32  | 
assistants, including Isabelle. Its main feature is script  | 
33  | 
management, providing a metaphor of stepwise proof script editing  | 
|
34  | 
and partial locking of the buffer.  | 
|
| 41596 | 35  | 
|
| 25214 | 36  | 
Other sources of information  | 
37  | 
||
38  | 
The Isabelle Page  | 
|
39  | 
||
40  | 
The Isabelle home page may be accessed both from Cambridge and Munich:  | 
|
| 27085 | 41  | 
* http://www.cl.cam.ac.uk/research/hvg/Isabelle/  | 
| 
25415
 
02884a4e1ac6
removed left-over text links from lynx conversion;
 
wenzelm 
parents: 
25214 
diff
changeset
 | 
42  | 
* http://isabelle.in.tum.de  | 
| 25214 | 43  | 
|
44  | 
Mailing list  | 
|
45  | 
||
46  | 
The electronic mailing list isabelle-users@cl.cam.ac.uk provides a  | 
|
| 25447 | 47  | 
forum for Isabelle users to discuss problems and exchange  | 
48  | 
information. To join, send a message to  | 
|
49  | 
isabelle-users-request@cl.cam.ac.uk.  | 
|
| 25214 | 50  | 
|
51  | 
Personal mail  | 
|
52  | 
||
| 
25415
 
02884a4e1ac6
removed left-over text links from lynx conversion;
 
wenzelm 
parents: 
25214 
diff
changeset
 | 
53  | 
Lawrence C Paulson  | 
| 25214 | 54  | 
Computer Laboratory  | 
55  | 
University of Cambridge  | 
|
56  | 
JJ Thomson Avenue  | 
|
57  | 
Cambridge CB3 0FD  | 
|
58  | 
England  | 
|
| 
25415
 
02884a4e1ac6
removed left-over text links from lynx conversion;
 
wenzelm 
parents: 
25214 
diff
changeset
 | 
59  | 
E-mail: lcp@cl.cam.ac.uk  | 
| 25214 | 60  | 
Phone: +44-223-763500  | 
61  | 
Fax: +44-223-334748  | 
|
62  | 
||
63  | 
or  | 
|
64  | 
||
| 
25415
 
02884a4e1ac6
removed left-over text links from lynx conversion;
 
wenzelm 
parents: 
25214 
diff
changeset
 | 
65  | 
Tobias Nipkow  | 
| 
 
02884a4e1ac6
removed left-over text links from lynx conversion;
 
wenzelm 
parents: 
25214 
diff
changeset
 | 
66  | 
Institut fuer Informatik  | 
| 
 
02884a4e1ac6
removed left-over text links from lynx conversion;
 
wenzelm 
parents: 
25214 
diff
changeset
 | 
67  | 
Technische Universitaet Muenchen  | 
| 25214 | 68  | 
Boltzmannstr. 3  | 
69  | 
D-85748 Garching  | 
|
70  | 
Germany  | 
|
| 
25415
 
02884a4e1ac6
removed left-over text links from lynx conversion;
 
wenzelm 
parents: 
25214 
diff
changeset
 | 
71  | 
E-mail: nipkow@in.tum.de  | 
| 25214 | 72  | 
Phone: +49-89-289-17302  | 
73  | 
Fax: +49-89-289-17307  | 
|
74  | 
_________________________________________________________________  | 
|
75  | 
||
76  | 
Please report any problems you encounter. While we shall try to be  | 
|
77  | 
helpful, we can accept no responsibility for the deficiencies of  | 
|
78  | 
Isabelle and their consequences.  | 
|
79  | 
_________________________________________________________________  |