# HG changeset patch # User wenzelm # Date 1214227885 -7200 # Node ID 904acdaf42996da47258a03b1cfba655702e4480 # Parent 385c0ce331737ad568cda34e5f1d2797230321bb induct_tac: mutual rules work as for method "induct"; diff -r 385c0ce33173 -r 904acdaf4299 NEWS --- a/NEWS Mon Jun 23 15:26:53 2008 +0200 +++ b/NEWS Mon Jun 23 15:31:25 2008 +0200 @@ -21,13 +21,15 @@ *** HOL *** -* 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. Old-style rules for mutual and -nested datatypes also need to be given explicitly. +* 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. * Attributes "cases", "induct", "coinduct" support "del" option.