author | Andreas Lochbihler |
Thu, 08 Aug 2013 18:20:15 +0200 | |
changeset 52917 | 2b68f4109075 |
parent 50572 | b33912e68b84 |
child 53525 | 3a58f2e249c7 |
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 |
|
50572 | 12 |
Isabelle works on the three main platform families: Linux, Windows, |
13 |
and Mac OS X. |
|
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 |
|
50572 | 24 |
Isabelle/jEdit is an advanced Prover IDE based on jEdit and |
25 |
Isabelle/Scala. It provides a metaphor of continuous proof |
|
26 |
checking of a versioned collection of theory sources, with |
|
44801 | 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 |
50572 | 33 |
management, with stepwise proof scripting and partial locking of |
34 |
the editor buffer. |
|
41596 | 35 |
|
25214 | 36 |
Other sources of information |
37 |
||
38 |
The Isabelle Page |
|
39 |
||
50572 | 40 |
The Isabelle home page may be accessed from Cambridge, Munich, and |
41 |
Sydney: |
|
42 |
||
27085 | 43 |
* http://www.cl.cam.ac.uk/research/hvg/Isabelle/ |
25415
02884a4e1ac6
removed left-over text links from lynx conversion;
wenzelm
parents:
25214
diff
changeset
|
44 |
* http://isabelle.in.tum.de |
50572 | 45 |
* http://mirror.cse.unsw.edu.au/pub/isabelle/index.html |
25214 | 46 |
|
47 |
Mailing list |
|
48 |
||
49 |
The electronic mailing list isabelle-users@cl.cam.ac.uk provides a |
|
25447 | 50 |
forum for Isabelle users to discuss problems and exchange |
51 |
information. To join, send a message to |
|
52 |
isabelle-users-request@cl.cam.ac.uk. |
|
25214 | 53 |
|
54 |
Personal mail |
|
55 |
||
25415
02884a4e1ac6
removed left-over text links from lynx conversion;
wenzelm
parents:
25214
diff
changeset
|
56 |
Lawrence C Paulson |
25214 | 57 |
Computer Laboratory |
58 |
University of Cambridge |
|
59 |
JJ Thomson Avenue |
|
60 |
Cambridge CB3 0FD |
|
61 |
England |
|
25415
02884a4e1ac6
removed left-over text links from lynx conversion;
wenzelm
parents:
25214
diff
changeset
|
62 |
E-mail: lcp@cl.cam.ac.uk |
25214 | 63 |
Phone: +44-223-763500 |
64 |
Fax: +44-223-334748 |
|
65 |
||
66 |
or |
|
67 |
||
25415
02884a4e1ac6
removed left-over text links from lynx conversion;
wenzelm
parents:
25214
diff
changeset
|
68 |
Tobias Nipkow |
02884a4e1ac6
removed left-over text links from lynx conversion;
wenzelm
parents:
25214
diff
changeset
|
69 |
Institut fuer Informatik |
02884a4e1ac6
removed left-over text links from lynx conversion;
wenzelm
parents:
25214
diff
changeset
|
70 |
Technische Universitaet Muenchen |
25214 | 71 |
Boltzmannstr. 3 |
72 |
D-85748 Garching |
|
73 |
Germany |
|
25415
02884a4e1ac6
removed left-over text links from lynx conversion;
wenzelm
parents:
25214
diff
changeset
|
74 |
E-mail: nipkow@in.tum.de |
25214 | 75 |
Phone: +49-89-289-17302 |
76 |
Fax: +49-89-289-17307 |
|
77 |
_________________________________________________________________ |
|
78 |
||
79 |
Please report any problems you encounter. While we shall try to be |
|
80 |
helpful, we can accept no responsibility for the deficiencies of |
|
81 |
Isabelle and their consequences. |
|
82 |
_________________________________________________________________ |