[isabelle-dev] NEWS

[Makarius]

* Methods "case_tac" and "induct_tac" now refer to the very same rule
declarations as the structured Isar versions "cases" and "induct", cf.
the corresponding "cases" and "induct" attributes.  INCOMPATIBILITY,
in rare situations a different rule is selected --- notably nested
tuple elimination instead of former prod.exhaust: use explicit
(case_tac t rule: prod.exhaust) here.

* Attributes "cases", "induct", "coinduct" support "del" option.