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