Re: [isabelle] Isabelle release candidate

... now with the attachment.


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)

2. Undoing a proof over an oops in a notepad context (as above) does not work
(at least with PG 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
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 - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft
theory Scratch imports Main begin

lemma Option_map_mono [partial_function_mono]:
  assumes "mono_option F"
  shows "mono_option (%f. 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"

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"
  "fooo iter G n queue =
   (case queue of [] => None
    | ((e', n') # queue') => 
      if n = n' then Some [e']
      else (Cons e') (fooo iter G n (queue @ map (\<lambda>e. (e, target G e)) (succs iter G n'))))"


notepad begin
  fix xs ys :: "'a list"
  have "xs = ys"
  proof(induction xs\<equiv>"xs" rule: list.induct)


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.