7 See the NEWS file in the distribution for details on user-relevant |
7 See the NEWS file in the distribution for details on user-relevant |
8 changes. |
8 changes. |
9 |
9 |
10 Installation |
10 Installation |
11 |
11 |
12 Isabelle works on the three main platform families: Linux, Mac OS |
12 Isabelle works on the three main platform families: Linux, Windows, |
13 X, and Windows (via Cygwin). |
13 and Mac OS X. |
14 |
14 |
15 Completely integrated bundles including the full Isabelle sources, |
15 Completely integrated bundles including the full Isabelle sources, |
16 documentation, add-on tools and precompiled logic images for |
16 documentation, add-on tools and precompiled logic images for |
17 several platforms are available from the Isabelle web page. |
17 several platforms are available from the Isabelle web page. |
18 |
18 |
19 Some background information may be found in the Isabelle System |
19 Some background information may be found in the Isabelle System |
20 Manual, distributed with the sources (directory doc). |
20 Manual, distributed with the sources (directory doc). |
21 |
21 |
22 User interfaces |
22 User interfaces |
23 |
23 |
24 Isabelle/jEdit is an emerging Prover IDE based on advanced |
24 Isabelle/jEdit is an advanced Prover IDE based on jEdit and |
25 technology of Isabelle/Scala. It provides a metaphor of continuous |
25 Isabelle/Scala. It provides a metaphor of continuous proof |
26 proof checking of a versioned collection of theory sources, with |
26 checking of a versioned collection of theory sources, with |
27 instantaneous feedback in real-time and rich semantic markup |
27 instantaneous feedback in real-time and rich semantic markup |
28 associated with the formal text. |
28 associated with the formal text. |
29 |
29 |
30 The classic Isabelle user interface is Proof General by David |
30 The classic Isabelle user interface is Proof General by David |
31 Aspinall and others. It is a generic Emacs interface for proof |
31 Aspinall and others. It is a generic Emacs interface for proof |
32 assistants, including Isabelle. Its main feature is script |
32 assistants, including Isabelle. Its main feature is script |
33 management, providing a metaphor of stepwise proof script editing |
33 management, with stepwise proof scripting and partial locking of |
34 and partial locking of the buffer. |
34 the editor buffer. |
35 |
35 |
36 Other sources of information |
36 Other sources of information |
37 |
37 |
38 The Isabelle Page |
38 The Isabelle Page |
39 |
39 |
40 The Isabelle home page may be accessed both from Cambridge and Munich: |
40 The Isabelle home page may be accessed from Cambridge, Munich, and |
|
41 Sydney: |
|
42 |
41 * http://www.cl.cam.ac.uk/research/hvg/Isabelle/ |
43 * http://www.cl.cam.ac.uk/research/hvg/Isabelle/ |
42 * http://isabelle.in.tum.de |
44 * http://isabelle.in.tum.de |
|
45 * http://mirror.cse.unsw.edu.au/pub/isabelle/index.html |
43 |
46 |
44 Mailing list |
47 Mailing list |
45 |
48 |
46 The electronic mailing list isabelle-users@cl.cam.ac.uk provides a |
49 The electronic mailing list isabelle-users@cl.cam.ac.uk provides a |
47 forum for Isabelle users to discuss problems and exchange |
50 forum for Isabelle users to discuss problems and exchange |