47 <p> <a href="http://www.polyml.org/">Poly/ML</a>, previously a |
47 <p> <a href="http://www.polyml.org/">Poly/ML</a>, previously a |
48 commercial product, is back in the free world. It is by far the best |
48 commercial product, is back in the free world. It is by far the best |
49 compiler for running Isabelle, requiring the least memory and offering |
49 compiler for running Isabelle, requiring the least memory and offering |
50 the highest performance. |
50 the highest performance. |
51 |
51 |
52 <p> <a |
52 <p> <a href="http://smlnj.sourceforge.net/">SML/NJ</a> needs more |
53 href="http://cm.bell-labs.com/cm/cs/what/smlnj/software.html">SML/NJ</a> |
53 store and disk space, but on the other hand supports more platforms. |
54 needs lots of store and disk space, but supports many more platforms. |
54 The current official release is 110. |
55 The current official release is 110. Basically, we still support the |
|
56 old 0.93 release, but do not recommend to use it under normal |
|
57 circumstances. |
|
58 |
55 |
59 <p> MLWorks used to be a commercial ML programming environment |
56 <p> MLWorks used to be a commercial ML programming environment |
60 developed by <a href="http://www.harlequin.com/">Harlequin</a> and was |
57 developed by <a href="http://www.harlequin.com/">Harlequin</a> and was |
61 unfortunately withdrawn after that company was taken over. Isabelle |
58 unfortunately withdrawn after that company was taken over. Isabelle |
62 on MLWorks 2.0 works reasonably well. |
59 on MLWorks 2.0 works reasonably well. |
63 |
60 |
64 |
61 |
65 <h2>Installation</h2> |
62 <h2>Installation</h2> |
66 |
63 |
67 Binary packages are available for Isabelle/HOL and ZF on the Linux/x86 |
64 Binary packages are available for Isabelle/HOL and ZF for several |
68 platform. The system may be easily built from scratch as well, taking |
65 platforms from the Isabelle web page. The system may be easily built |
69 the traditional tar.gz source distribution. See file <tt>INSTALL</tt> |
66 from scratch as well, taking the traditional tar.gz source |
70 as distributed with Isabelle for more information. |
67 distribution. See file <tt>INSTALL</tt> as distributed with Isabelle |
|
68 for more information. |
71 |
69 |
72 Further background information may be found in the <em>Isabelle System |
70 Further background information may be found in the <em>Isabelle System |
73 Manual</em>, distributed with the sources (directory <tt>doc</tt>). |
71 Manual</em>, distributed with the sources (directory <tt>doc</tt>). |
74 |
72 |
75 |
73 |
85 recently gained a rather large following of both beginning and expert |
83 recently gained a rather large following of both beginning and expert |
86 users of Isabelle. |
84 users of Isabelle. |
87 |
85 |
88 <p> |
86 <p> |
89 |
87 |
90 Proof General may be used together with the Emacs |
88 Proof General is distributed together with the XEmacs |
91 <a href="http://x-symbol.sourceforge.net"> |
89 <a href="http://x-symbol.sourceforge.net"> |
92 X-Symbol package</a>, which provides a nice way to get proper |
90 X-Symbol package</a>, which provides a nice way to get proper |
93 mathematical symbols displayed on screen. |
91 mathematical symbols displayed on screen. |
94 |
92 |
95 |
93 |