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

notepad begin
  fix xs ys :: "'a list"
  have "xs = ys"
  proof(induction xs=="xs" rule: list.induct)
    print_cases
    oops
end

2. Undoing a proof over an oops in a notepad context (as above) does not work (at least with PG 3.7.1.1. 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.

Andreas


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:

http://isabelle.in.tum.de/website-Isabelle2011-1-RC1/

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.


Makarius


--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
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 MHonArc.