[isabelle-dev] default cases rule

[Dmitriy Traytel]

Hi Chris,

Am 05.09.2014 um 12:27 schrieb Christian Sternagel:
> [...]
>
> First question: is this intentional and what is the current default rule?
Yes. Quoting from the news:

>     The rule "set_cases" is now registered with the "[cases set]"
>     attribute. This can influence the behavior of the "cases" proof
>     method when more than one case rule is applicable (e.g., an
>     assumption is of the form "w : set ws" and the method "cases w"
>     is invoked). The solution is to specify the case rule explicitly
>     (e.g. "cases w rule: widget.exhaust").
>     INCOMPATIBILITY.

> Second question: is it considered "bad form" to rely on default rules?
No, I think it's fine. Such (radical) changes of definitions (set in 
this case) are seldom.

Dmitriy