34 <p> |
34 <p> |
35 |
35 |
36 |
36 |
37 <h2>Obtaining Isabelle</h2> |
37 <h2>Obtaining Isabelle</h2> |
38 |
38 |
39 Visit the <a href="dist/">download page</a>. |
39 See the <a href="dist/">download page</a>. |
40 <p> |
40 <p> |
41 Several mirror sites provide the Isabelle <a |
41 |
42 href="dist/">distribution</a>, which includes <a |
42 Several mirror sites provide the Isabelle <a |
43 href="dist/source.html">sources</a>, <a |
43 href="dist/">distribution</a>, which includes source and binary <a |
44 href="dist/binary.html">binary packages</a>, and <a |
44 href="dist/packages.html">packages</a> and browsable <a |
45 href="dist/docs.html">documentation</a>. |
45 href="dist/docs.html">documentation</a>. The current version is |
46 The current version is <strong><!-- _GP_ distname --></strong>. |
46 <strong><!-- _GP_ distname --></strong>. |
47 |
47 |
48 <p> |
48 <p> |
49 |
49 |
50 You can also browse the main Isabelle logics |
50 You can also browse the Isabelle theory <a href="library">library</a>; |
51 <a href="library/HOL/">HOL</a>, <a href="library/HOLCF/">HOLCF</a>, |
51 the main logics are <a href="library/HOL/">HOL</a>, <a |
52 <a href="library/FOL/">FOL</a> and <a href="library/ZF/">ZF</a> online. |
52 href="library/HOLCF/">HOLCF</a>, <a href="library/FOL/">FOL</a> and <a |
53 |
53 href="library/ZF/">ZF</a>. |
54 <p> |
|
55 |
|
56 |
|
57 <h2>User interface</h2> |
|
58 |
|
59 The distribution includes only a very primitive interface based on |
|
60 ordinary terminal sessions. |
|
61 |
|
62 <p> |
|
63 |
|
64 <a href="http://zermelo.dcs.ed.ac.uk/~proofgen/">Proof General</a> is |
|
65 a generic Emacs interface for proof assistants, including Isabelle |
|
66 (both for the classic and Isar version). Proof General is suitable |
|
67 for use by pacifists and Emacs militants alike. Its most prominent |
|
68 feature is script management, providing a metaphor of <em>live proof |
|
69 script editing</em>. |
|
70 |
54 |
71 <p> |
55 <p> |
72 |
56 |
73 |
57 |
74 <h2>Mailing list</h2> |
58 <h2>Mailing list</h2> |
75 |
59 |
76 Use the mailing list <a href="mailto: |
60 Use the mailing list <a href="mailto: |
77 isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> to |
61 isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> to |
78 discuss problems and results. |
62 discuss problems and results. Why not <A |
79 (Why not <A HREF="mailto:lcp@cl.cam.ac.uk">subscribe</A>?) |
63 HREF="mailto:lcp@cl.cam.ac.uk">subscribe</A>? |