[isabelle-dev] Towards the Isabelle2014 release
Thomas Sewell
thomas.sewell at nicta.com.au
Wed Jun 4 07:27:16 CEST 2014
I had hoped to have the change I was making to hypothesis-substitution
ready for the coming release.
I've got it working for all of HOL and the library, and begun looking at
the AFP and at the l4.verified proofs. The HOL+library changes were easy
enough, but the l4.verified changes are somewhat daunting and I haven't
gotten anywhere with the AFP yet.
I'll have another look at it, because I'd like this to go somewhere at
some point. It might have to wait for a subsequent release though.
Cheers,
Thomas.
On 30/05/14 21:30, Makarius wrote:
> The summer is getting close, and we need to start thinking about the
> coming release.
>
> I am myself on vacation during most of June. On return I would like to
> wrap up rather quickly, so that we can publish Isabelle2014-RC0 in the
> second week of July, for the Isabelle tutorial at VSL2014 Vienna.
> That will be still within the main Isabelle repository.
>
> The usual fork to the release repository and the regular sequence of
> Isabelle2014-RC1, RC2, RC3, ... will happen in the week after ITP 2014.
>
> I am myself attending the mega event at Vienna 13..19-Jul-2014. This
> will be also an opportunity to show me personally remaining snags, and
> to continue the elimination of remaining uses of Proof General. (It
> is getting harder and harder to construct counter-examples to the
> claim that this set is already empty.)
>
>
> Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
More information about the isabelle-dev
mailing list