`My guess would be that a non-empty decoration is possible for`

`Z'SchemaPred to allow for variable decoration during proof operations:`

`if all variables in the characteristic binding are consistently`

`decorated, the resulting term is still Z.`

`However, not all Z proof operations consistently decorate the variables`

`in the characteristic binding, so the semantic constant Z'SchemaPred is`

`exposed fairly often. (This could be avoided with schema renaming as`

`already done recently.)`

Phil On 24/09/11 13:09, Rob Arthan wrote:

Phil, On 17 Sep 2011, at 15:06, Phil Clayton wrote:Using the subgoal package, I have just been trying to quote an assumption (as a term quotation) but couldn't. On the assumption term, dest_z_term returns the form ZSchemaPred (..., "'") Given, e.g. (* S : P [a, b : Z] *) val S = %SZT% S %bigcolon% %bbP% [a, b : %bbZ%] %>%; is there a way to write a Z term quotation equal to tm1 as follows: val tm1 = mk_z_schema_pred (S, "'"); ? (I can do so in HOL using Z'SchemaPred directly.)The quick answer is no - the term generator (imp063.doc) never calls mk_z_schema_pred with non-empty decoration. I need to remind myself exactly what the decoration in mk_z_schema_pred is for (I know what the semantics is intended to be but I can't recall why we have it). Perhaps Roger can cast his mind back to this. This reminds me that I always meant to make the Z specifications of the Z to HOL mapping available. As a quick fix, I have put the documents here: http://dl.dropbox.com/u/34693999/zed002.pdf http://dl.dropbox.com/u/34693999/zed003.pdf http://dl.dropbox.com/u/34693999/zed005.pdf I will make sure they typecheck presently and include them in the doc directory in future builds. Regards, Rob. _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com