[isabelle-dev] default cases rule

Christian Sternagel c.sternagel at gmail.com
Fri Sep 5 15:50:19 CEST 2014

Thanks for your replies!

I forgot to check the NEWS ;)

For the record: the change affected in the order of 10 proofs in IsaFoR 
(most of which unnecessarily chained facts into the cases method) which 
where of course trivially repaired.



On 09/05/2014 02:48 PM, Jasmin Christian Blanchette wrote:
> 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

More information about the isabelle-dev mailing list