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
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