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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
