There appears to be a bug in z_%mem%_seta_conv (see attached) when renaming of bound variables is required but the bound variables are introduced by a schema declaration.

I'm guessing this is the reason that stripping is not working in my proof (see attached). It looks trivial but I can't see a way to finish it without getting stuck into the HOL embedding. (As shown, renaming the schema components partially helps.) Can anyone think of a Z work-around for now?


Attachment: z_%mem%_seta_conv_issue.sml.gz
Description: GNU Zip compressed data

Proofpower mailing list

Reply via email to