[isabelle-dev] default cases rule

[Christian Sternagel]

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.

cheers

chris

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
>