On Sat, Apr 28, 2012 at 9:48 AM, Florian Haftmann <[email protected]> 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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
