equal
deleted
inserted
replaced
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 work on the three main platform families: Linux, Mac OS X, |
12 Isabelle works on the three main platform families: Linux, Mac OS |
13 and Windows (via Cygwin). |
13 X, and Windows (via Cygwin). |
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 |
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 most prominent feature is |
32 assistants, including Isabelle. Its main feature is script |
33 script management, providing a metaphor of stepwise proof script |
33 management, providing a metaphor of stepwise proof script editing |
34 editing. |
34 and partial locking of the 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 |