33 archives, research papers, the Isabelle bibliography, and Isabelle |
33 archives, research papers, the Isabelle bibliography, and Isabelle |
34 workshops and courses. |
34 workshops and courses. |
35 |
35 |
36 <p> |
36 <p> |
37 |
37 |
|
38 <h2><!-- _GP_ distname --></h2> |
|
39 New features in <strong><!-- _GP_ distname --></strong> include |
|
40 <ul> |
|
41 <li>New theory Ring_and_Field with over 250 basic numerical laws, |
|
42 all proved in axiomatic type classes for semirings, rings and fields.</li> |
|
43 |
|
44 <li>New locale <code>ring</code> for non-commutative rings in HOL-Algebra.</li> |
|
45 |
|
46 <li>Type <code>rat</code> of the rational numbers available in HOL-Complex.</li> |
|
47 |
|
48 <li>Improved locales (named proof contexts), instantiation of locales.</li> |
|
49 |
|
50 <li>Improved calculational reasoning chains.</li> |
|
51 |
|
52 <li>Improved records handling.</li> |
|
53 |
|
54 <li>Improved handling of linear and partial orders in simplifier.</li> |
|
55 |
|
56 <li>New <code>specification</code> command for definition by specification.</li> |
|
57 |
|
58 <li>New Isar command <code>finalconsts</code> prevents constants being given a definition later.</li> |
|
59 |
|
60 <li><code>arith</code> now generates counterexamples for reals as well.</li> |
|
61 |
|
62 <li>New <code>refute</code> command to search for (finite) countermodels for a fragment of HOL.</li> |
|
63 |
|
64 <li>Presentation and x-symbol enhancements, greek letters and sub/superscripts in identifiers.</li> |
|
65 </ul> |
|
66 <a href="dist/<!-- _GP_ distname -->/NEWS">[Complete Changelog]</a> |
|
67 <p> |
|
68 The <strong><!-- _GP_ distname --></strong> distribution is available |
|
69 from several <a href="dist/index.html">mirror sites</a>. It includes |
|
70 source and binary packages and browsable documentation. There is also |
|
71 a nightly generated <a href="http://isabelle.in.tum.de/devel/">development |
|
72 snapshot</a> available. |
|
73 |
|
74 <p> |
|
75 |
38 <h2>Out now</h2> |
76 <h2>Out now</h2> |
39 |
77 |
40 The |
78 The |
41 <a href="dist/<!-- _GP_ distname -->/doc/tutorial.pdf">Tutorial on Isabelle/HOL</a> -- |
79 <a href="dist/<!-- _GP_ distname -->/doc/tutorial.pdf">Tutorial on Isabelle/HOL</a> -- |
42 published by Springer Verlag as <a |
80 published by Springer Verlag as <a |
43 href="http://www4.in.tum.de/~nipkow/LNCS2283/">LNCS 2283</a>. |
81 href="http://www4.in.tum.de/~nipkow/LNCS2283/">LNCS 2283</a>. |
44 |
|
45 <p> |
|
46 |
|
47 <h2>Obtaining Isabelle</h2> |
|
48 |
|
49 The <strong><!-- _GP_ distname --></strong> distribution is available |
|
50 from several <a href="dist/index.html">mirror sites</a>. It includes |
|
51 source and binary packages and browsable documentation. There is also |
|
52 a nightly generated <a href="http://isabelle.in.tum.de/devel/">development |
|
53 snapshot</a> available. |
|
54 |
82 |
55 <p> |
83 <p> |
56 |
84 |
57 You can also browse the <a href="library/index.html">Isabelle theory |
85 You can also browse the <a href="library/index.html">Isabelle theory |
58 library</a>; the main logics are <a |
86 library</a>; the main logics are <a |