author | wenzelm |
Wed, 14 Feb 2024 14:41:18 +0100 | |
changeset 79604 | 0e8ac7db1f4d |
parent 73530 | 89cf7c903aca |
permissions | -rw-r--r-- |
71336 | 1 |
The Isabelle System Distribution |
2 |
================================ |
|
25214 | 3 |
|
73530 | 4 |
See the NEWS file in the distribution for details on user-relevant |
5 |
changes. The ANNOUNCE file recounts notable changes for the latest |
|
6 |
official release. |
|
25214 | 7 |
|
73530 | 8 |
The core of Isabelle is subject to a 3-clause BSD license, but add-on |
9 |
components have their own license schemes (similar to a Linux |
|
10 |
distribution). |
|
71336 | 11 |
|
25214 | 12 |
|
47795
ccb10fe4b955
some updates on classic README, reduce the impression that there is much to install manually;
wenzelm
parents:
47745
diff
changeset
|
13 |
Installation |
71336 | 14 |
------------ |
33842 | 15 |
|
71336 | 16 |
Isabelle works on the three main platform families: Linux, Windows, |
17 |
and macOS. The application bundles from the Isabelle web page |
|
18 |
include sources, documentation, and add-on tools for all supported |
|
19 |
platforms. |
|
25214 | 20 |
|
71336 | 21 |
Some technical background information may be found in the Isabelle |
22 |
System Manual (directory doc). |
|
23 |
||
25214 | 24 |
|
57452 | 25 |
User interface |
71336 | 26 |
-------------- |
25214 | 27 |
|
71336 | 28 |
Isabelle/jEdit is an advanced Prover IDE based on jEdit and |
29 |
Isabelle/Scala. It is the main example application of the |
|
30 |
Isabelle/PIDE framework, and the default user interface of |
|
31 |
Isabelle. It provides a metaphor of continuous proof checking of a |
|
32 |
versioned collection of theory sources, with instantaneous feedback |
|
33 |
in real-time and rich semantic markup associated with the formal |
|
34 |
text. |
|
35 |
||
41596 | 36 |
|
25214 | 37 |
Other sources of information |
71336 | 38 |
---------------------------- |
25214 | 39 |
|
71336 | 40 |
* The Isabelle Page |
41 |
||
42 |
The Isabelle home page may be accessed from the following mirror |
|
43 |
sites: |
|
50572 | 44 |
|
68649 | 45 |
* https://www.cl.cam.ac.uk/research/hvg/Isabelle |
46 |
* https://isabelle.in.tum.de |
|
70025 | 47 |
* https://mirror.cse.unsw.edu.au/pub/isabelle |
68649 | 48 |
* https://mirror.clarkson.edu/isabelle |
25214 | 49 |
|
71336 | 50 |
* Mailing list |
25214 | 51 |
|
71336 | 52 |
The electronic mailing list isabelle-users@cl.cam.ac.uk provides a |
53 |
forum for Isabelle users to discuss problems and exchange |
|
54 |
information. To join, send a message to |
|
55 |
isabelle-users-request@cl.cam.ac.uk. |
|
25214 | 56 |
|
71336 | 57 |
* Personal mail |
25214 | 58 |
|
71336 | 59 |
Lawrence C Paulson |
60 |
Computer Laboratory |
|
61 |
University of Cambridge |
|
62 |
JJ Thomson Avenue |
|
63 |
Cambridge CB3 0FD |
|
64 |
England |
|
65 |
E-mail: lcp@cl.cam.ac.uk |
|
66 |
Phone: +44-223-763500 |
|
67 |
Fax: +44-223-334748 |
|
25214 | 68 |
|
71336 | 69 |
or |
25214 | 70 |
|
71336 | 71 |
Tobias Nipkow |
71337 | 72 |
Institut für Informatik |
73 |
Technische Universität München |
|
71336 | 74 |
Boltzmannstr. 3 |
75 |
D-85748 Garching |
|
76 |
Germany |
|
77 |
E-mail: nipkow@in.tum.de |
|
78 |
Phone: +49-89-289-17302 |
|
79 |
Fax: +49-89-289-17307 |
|
25214 | 80 |
|
71336 | 81 |
NOTE: |
82 |
Please report any problems you encounter. While we shall try to be |
|
83 |
helpful, we can accept no responsibility for the deficiencies of |
|
84 |
Isabelle and their consequences. |