[isabelle-dev] default cases rule
Jasmin Christian Blanchette
jasmin.blanchette at gmail.com
Fri Sep 5 14:48:00 CEST 2014
>> 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