Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes

> On 19.11.2015, at 00:15, Makarius <makarius at> wrote:
> On Wed, 18 Nov 2015, Jasmin Blanchette wrote:
>> Overall, we managed to achieve very high levels of backward compatibility and actually pulled it off. The ongoing "Nominal2" vs. "Nominal" is reminder of how hard it is to subsume and replace an existing Isabelle package. We (I) have made bona fide errors along the way, but I think our record is remarkable and deserves more praise than criticism.
> Definitely.  I am impressed how the BNF datatype upgrade went through, while the task was looking bigger and bigger as the years passed by.  One of the greatest engineering projects since Stonehenge!

Tobias already clarified what he was aiming at, but let me chime in to say that I also was impressed with how professionally the new BNF datatypes were introduced and with the prompt support I got from Jasmin and everyone involved to help iron out the few issues it raised in our proofs.

It does deserve praise, I donât think anyone doubts that.



The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.