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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
