*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Isabelle release candidate*From*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Date*: Wed, 28 Sep 2011 17:56:36 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <4E834369.7050406@kit.edu>*References*: <alpine.LNX.1.10.1109270007280.450@atbroy100.informatik.tu-muenchen.de> <4E834369.7050406@kit.edu>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.13) Gecko/20101208 Thunderbird/3.1.7

... now with the attachment. Andreas Am 28.09.2011 17:55, schrieb Andreas Lochbihler:

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

theory Scratch imports Main begin lemma Option_map_mono [partial_function_mono]: assumes "mono_option F" shows "mono_option (%f. Option.map g (F f))" by(rule monotoneI)(auto simp add: flat_ord_def dest!: monotoneD[OF assms]) type_synonym ('mdigraph, 'node, 'edge, 's) mdigraph_iter = "'mdigraph => ('s => bool) => ('edge => 's => 's) => 'node => 's => 's" locale test = fixes target :: "'mdigraph => 'edge => 'node" begin definition succs :: "('mdigraph, 'node, 'edge, 'edge list) mdigraph_iter => 'mdigraph => 'node => 'edge list" where "succs = undefined" partial_function (option) foo :: "('mdigraph, 'node, 'edge, 'edge list) mdigraph_iter => 'mdigraph => 'node => ('edge * 'node) list => 'edge list option" where "fooo iter G n queue = (case queue of [] => None | ((e', n') # queue') => if n = n' then Some [e'] else Option.map (Cons e') (fooo iter G n (queue @ map (\<lambda>e. (e, target G e)) (succs iter G n'))))" end notepad begin fix xs ys :: "'a list" have "xs = ys" proof(induction xs\<equiv>"xs" rule: list.induct) print_cases oops end end

**References**:**[isabelle] Isabelle release candidate***From:*Makarius

**Re: [isabelle] Isabelle release candidate***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Isabelle release candidate
- Next by Date: Re: [isabelle] Isabelle release candidate
- Previous by Thread: Re: [isabelle] Isabelle release candidate
- Next by Thread: Re: [isabelle] Isabelle release candidate
- Cl-isabelle-users September 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list