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

[Brian Huffman]

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