[isabelle-dev] Strange line in NEWS [was: Isabelle release test website]

Brian Huffman huffman at in.tum.de
Sat Apr 28 09:56:28 CEST 2012

On Sat, Apr 28, 2012 at 9:48 AM, Florian Haftmann
<florian.haftmann at informatik.tu-muenchen.de> wrote:
> Hi Christian,
>> I spotted this strange line in the NEWS (linked from the test website)
>>   symp_def ~> (dropped, use symp_def and sym_def instead)
> the LHS is before, the RHS is after the change.  In particular, the
> symp_def from the RHS is another one than that form the LHS.

It is confusing/wrong to say that symp_def was "dropped" when we still
have a theorem by that name.

Perhaps the line should read something like this:

symp_def ~> (modified, use new symp_def and sym_def instead)

- Brian

More information about the isabelle-dev mailing list