[isabelle-dev] default cases rule
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. ;)
More information about the isabelle-dev