[isabelle-dev] Strange line in NEWS [was: Isabelle release test website]
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)
More information about the isabelle-dev