[isabelle-dev] Towards the Isabelle2014 release

[Thomas Sewell]

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 
>