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:

I will make sure they typecheck presently and include them in the doc directory 
in future builds.



Proofpower mailing list

Reply via email to