* 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.
