Re: [isabelle] Isabelle release candidate
I have found the following inconveniences in the release candidate, but I
consider none of them as release critical.
1. The new induction method does not give the induction hypothesis the name IH
(as advertised in the NEWS) when explicit parameter instantiations are given.
Here's a silly example
fix xs ys :: "'a list"
have "xs = ys"
proof(induction xs=="xs" rule: list.induct)
2. Undoing a proof over an oops in a notepad context (as above) does not work
(at least with PG 220.127.116.11. and XEmacs; I haven't tested the other interfaces).
3. partial_function sometimes does not check that the head of the equation is
the same as the name of the constant to be defined, as in the attached example.
Am 27.09.2011 00:20, schrieb Makarius:
The next official Isabelle release is scheduled for October 2011. In the 2-3
weeks before shipment there are traditional test releases, but this time they
are called "release candidates" and announced to a wider audience.
So Isabelle2011-1-RC1 is now available here:
This enables users to try on their own machines, and see how their applications
work with the coming release. Incompatibilites between the RCs and the final
version should be neglibile.
This gives an opportunity for last-minute fixes, but no feature additions (the
de-facto feature freeze is usually 6 weeks before a release, so it is long over).
Feedback on problems can be posted on the list, or sent privately.
Karlsruher Institut für Technologie
Adenauerring 20a, Geb. 50.41, Raum 031
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
in der Helmholtz-Gemeinschaft
This archive was generated by a fusion of
Pipermail (Mailman edition) and