Re: [isabelle] Isabelle2016-RC0 - AFP and Library available for testing

On Mon, 11 Jan 2016, Gerwin Klein wrote:

There are some theories it depends on that donât work yet, but WordLemmaBucket should be usable without those (they are mostly some Eisbach tweaks that still need updating and are possibly obsolete for Isabelle2016).

During the update I found we had a few instance of this pattern:

 lemmas x = y [where a = b, simplified]

This fails with an error message in Isabelle2016-RC0. I used this idiom instead:

 lemmas x' = y [where a = b]
 lemmas x = x' [simplified]

Is this what I should be doing, or is there a nicer way without introducing an x'?

Is that the "where" attribute of Eisbach or Pure?

The Eisbach version was fluctuating a bit in the past few months. In Isabelle2016-RC1 it is again closer to the Pure version.

The full re-unification of both variants has to wait for another release.


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