[isabelle-dev] NEWS update

[Makarius]

* Methods "case_tac" and "induct_tac" now refer to the very same rules
as the structured Isar versions "cases" and "induct", cf. the
corresponding "cases" and "induct" attributes.  Mutual induction rules
are now presented as a list of individual projections
(e.g. foo_bar.inducts for types foo and bar); the old format with
explicit HOL conjunction is no longer supported.  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.