author | wenzelm |
Fri, 23 Mar 2018 14:04:50 +0100 | |
changeset 67931 | f7917c15b566 |
parent 67866 | 11e4060bcdca |
child 68649 | f849fc1cb65e |
permissions | -rw-r--r-- |
25214 | 1 |
The Isabelle System Distribution |
2 |
||
3 |
Version information |
|
4 |
||
67866 | 5 |
This is some 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, |
53978 | 13 |
and Mac OS X. The application bundles from the Isabelle web page |
14 |
include sources, documentation, and add-on tools for all supported |
|
15 |
platforms. |
|
25214 | 16 |
|
54051 | 17 |
Some technical background information may be found in the Isabelle |
18 |
System Manual (directory doc). |
|
25214 | 19 |
|
57452 | 20 |
User interface |
25214 | 21 |
|
50572 | 22 |
Isabelle/jEdit is an advanced Prover IDE based on jEdit and |
57452 | 23 |
Isabelle/Scala. It is the main example application of the |
24 |
Isabelle/PIDE framework, and the default user interface of |
|
25 |
Isabelle. It provides a metaphor of continuous proof checking of a |
|
26 |
versioned collection of theory sources, with instantaneous feedback |
|
27 |
in real-time and rich semantic markup associated with the formal |
|
28 |
text. |
|
41596 | 29 |
|
25214 | 30 |
Other sources of information |
31 |
||
32 |
The Isabelle Page |
|
33 |
||
62197 | 34 |
The Isabelle home page may be accessed from the following mirror |
35 |
sites: |
|
50572 | 36 |
|
62190 | 37 |
* http://www.cl.cam.ac.uk/research/hvg/Isabelle |
25415
02884a4e1ac6
removed left-over text links from lynx conversion;
wenzelm
parents:
25214
diff
changeset
|
38 |
* http://isabelle.in.tum.de |
62190 | 39 |
* http://mirror.cse.unsw.edu.au/pub/isabelle |
62197 | 40 |
* http://mirror.clarkson.edu/isabelle |
25214 | 41 |
|
42 |
Mailing list |
|
43 |
||
44 |
The electronic mailing list isabelle-users@cl.cam.ac.uk provides a |
|
25447 | 45 |
forum for Isabelle users to discuss problems and exchange |
46 |
information. To join, send a message to |
|
47 |
isabelle-users-request@cl.cam.ac.uk. |
|
25214 | 48 |
|
49 |
Personal mail |
|
50 |
||
25415
02884a4e1ac6
removed left-over text links from lynx conversion;
wenzelm
parents:
25214
diff
changeset
|
51 |
Lawrence C Paulson |
25214 | 52 |
Computer Laboratory |
53 |
University of Cambridge |
|
54 |
JJ Thomson Avenue |
|
55 |
Cambridge CB3 0FD |
|
56 |
England |
|
25415
02884a4e1ac6
removed left-over text links from lynx conversion;
wenzelm
parents:
25214
diff
changeset
|
57 |
E-mail: lcp@cl.cam.ac.uk |
25214 | 58 |
Phone: +44-223-763500 |
59 |
Fax: +44-223-334748 |
|
60 |
||
61 |
or |
|
62 |
||
25415
02884a4e1ac6
removed left-over text links from lynx conversion;
wenzelm
parents:
25214
diff
changeset
|
63 |
Tobias Nipkow |
02884a4e1ac6
removed left-over text links from lynx conversion;
wenzelm
parents:
25214
diff
changeset
|
64 |
Institut fuer Informatik |
02884a4e1ac6
removed left-over text links from lynx conversion;
wenzelm
parents:
25214
diff
changeset
|
65 |
Technische Universitaet Muenchen |
25214 | 66 |
Boltzmannstr. 3 |
67 |
D-85748 Garching |
|
68 |
Germany |
|
25415
02884a4e1ac6
removed left-over text links from lynx conversion;
wenzelm
parents:
25214
diff
changeset
|
69 |
E-mail: nipkow@in.tum.de |
25214 | 70 |
Phone: +49-89-289-17302 |
71 |
Fax: +49-89-289-17307 |
|
72 |
_________________________________________________________________ |
|
73 |
||
74 |
Please report any problems you encounter. While we shall try to be |
|
75 |
helpful, we can accept no responsibility for the deficiencies of |
|
76 |
Isabelle and their consequences. |
|
77 |
_________________________________________________________________ |