On 25/09/11 10:04, Roger Bishop Jones wrote:
On Saturday 24 Sep 2011 22:53, Roger Bishop Jones wrote:
On Saturday 24 Sep 2011 13:09, Rob Arthan wrote:
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
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 decora
On Saturday 24 Sep 2011 22:53, Roger Bishop Jones wrote:
> On Saturday 24 Sep 2011 13:09, Rob Arthan wrote:
> > 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_sc
