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



> On 17 Jan 2016, at 12:19 AM, Makarius <makarius at sketis.net> wrote:
>
> 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?

This is indeed the Eisbach âwhere", which WordLemmaBucket happened to use due to it depending on Eisbach in our theory layout. The theory now checks in Isabelle2016-RC1 without rewriting any attribute expressions.

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


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.


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