[isabelle-dev] default cases rule
traytel at in.tum.de
Fri Sep 5 12:53:36 CEST 2014
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").
> 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.
More information about the isabelle-dev