[isabelle-dev] default cases rule

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Fri Sep 5 14:48:00 CEST 2014

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



More information about the isabelle-dev mailing list