[isabelle] Isabelle2016-1-RC0 AFP and small user experience



Hi,

is there already a working version of the afp theory
"Automatic_Refinement/Lib/Misc.thy" available?

How long will the merge window for the afp be? I'd like to update my
entries.

By the way, a small first user experience:
I noticed that when I have a theorem name such as
"Complete_Lattices.UN_empty2" and I double click it, it does not select the
whole name but only either the first part "Complete_Lattices" or the second
part "UN_empty2". So far, selecting the complete name by a double click
felt more convenient to me, but probably a bigger change happend to
Isabelle2016-1 which makes the new behavior the 'better' one.

Best,
  Cornelius

2016-10-07 10:10 GMT+02:00 Makarius <makarius at sketis.net>:

> Dear Isabelle users,
>
> the year 2016 is an "Isabelle leap-year", with more than one release.
> (The usual distance between regular releases is 8-10 months.)
>
> Many changes and improvements have been accumulated in the past few
> months. A preview of what is coming is available here:
> http://isabelle.in.tum.de/website-Isabelle2016-1-RC0
>
> This corresponds to Isabelle/666c7475f4f7 and AFP/1e958cc1942e. Note
> that the website and documentation still need to be updated.
>
>
> Despite the name "Isabelle2016-1", this is not a revised version of
> Isabelle2016, but a completely new major release. See also
> the NEWS file
> http://isabelle.in.tum.de/website-Isabelle2016-1-RC0/
> dist/Isabelle2016-1-RC0/doc/NEWS.html
>
> When discussing problems, observations, suggestions, etc. the mail
> subject line should be changed to something meaningful (but the release
> candidate number still given in the message body).
>
>
>         Makarius
>
>



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