On 28 Jul 2011, at 18:10, Phil Clayton wrote:

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.

Yes. This needs to be fixed.

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?

I have attached a work-around where the mixed language working is not too bad (you don't see any semantic constants). Higher-order matching saves a little bit of pain in this.



Attachment: forphilc110730.tgz
Description: Binary data

Proofpower mailing list

Reply via email to