| author | wenzelm | 
| Sat, 04 Mar 2023 16:45:21 +0100 | |
| changeset 77505 | 7ee426daafa3 | 
| 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.  |