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.)
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
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
