Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] [ExternalEmail] datatype_compat in Isabelle201...


view this post on Zulip Email Gateway (Aug 22 2022 at 17:24):

From: Gerwin.Klein@data61.csiro.au
Well, that turned out to something mildly embarrassing. Since the definition of dt_pair is in a different theory, I had forgotten to remove the (plugins del: size) part there as well. If I do that, the fun definitions do go through.

Thanks, Dmitriy for pointing that out.

There are later proofs that then break, but I’ve bitten the bullet and updated those to what comes out of the new datatype package. The image builds fine and the direct tests on top seem to be fine as well, so it’s looking good so far.

Cheers,
Gerwin


Last updated: Mar 29 2024 at 08:18 UTC