[isabelle-dev] default cases rule

[Jasmin Christian Blanchette]

Hi all,

Dmitriy wrote:

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

I would like to add that this "radical" change broke only a handful of proofs in the AFP, i.e., it was not so radical after all. ;)

Cheers,

Jasmin