`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 (..., "'")

## Advertising

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.) All my attempts result in a term equal to tm2 as follows: val tm2 = mk_z_schema_pred (mk_z_decor%down%s (S, "'"), "");

`tm1 and tm2 are equivalent so this is hardly an issue for writing Z`

`specifications but can make quoting terms awkward. In the end, I just`

`referred to the assumption by index.`

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