43 mailing list archives, research papers, the Isabelle |
43 mailing list archives, research papers, the Isabelle |
44 bibliography, and Isabelle workshops and courses. |
44 bibliography, and Isabelle workshops and courses. |
45 </p> |
45 </p> |
46 |
46 |
47 <h2>Now available: Isabelle 2005</h2> |
47 <h2>Now available: Isabelle 2005</h2> |
48 <p>Some notable highlights:</p> |
48 <p>Some notable features:</p> |
49 <ul> |
49 <ul> |
50 <li>Interpretation of locale expressions in theories, locales, and proof contexts.</li> |
50 <li>Interpretation of locale expressions in theories, locales, and proof contexts.</li> |
51 <li>Substantial library improvements (HOL, HOL-Complex, HOLCF).</li> |
51 <li>Substantial library improvements (HOL, HOL-Complex, HOLCF).</li> |
52 <li>Proof tools for transitivity reasoning.</li> |
52 <li>Proof tools for transitivity reasoning.</li> |
53 <li>General <code>find_theorems</code> command (by term patterns, as intro/elim/simp rules etc.).</li> |
53 <li>General <code>find_theorems</code> command (by term patterns, as intro/elim/simp rules etc.).</li> |
54 <li>Commands for generating adhoc draft documents.</li> |
54 <li>Commands for generating adhoc draft documents.</li> |
55 <li>Support for Unicode proof documents (UTF-8).</li> |
55 <li>Support for Unicode proof documents (UTF-8).</li> |
56 <li>Major internal reorganizations and performance improvements.</li> |
56 <li>Major internal reorganizations and performance improvements.</li> |
|
57 <li>More well-formedness checks of overloaded |
|
58 definitions, but fails to recognize certain ill-formed definitions |
|
59 that Isabelle2004 would have rejected outright!</li> |
57 </ul> |
60 </ul> |
58 |
61 |
59 <p><a href="//dist/Isabelle/NEWS">[Cumulative NEWS]</a></p> |
62 <p><a href="//dist/Isabelle/NEWS">[Cumulative NEWS]</a></p> |
60 |
63 |
61 <h2>Download</h2> |
64 <h2>Download</h2> |