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_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.

My memory is pretty bad on the history.

I expect that I started out with the syntax in Spivey's "The 
Z Notation" (It was the only game in town at the time).
But then you might expect to see "gen actuals" and 
"renaming!" there.

To unravel it one would need to look at the very early 
editions of the specification.
Do the SCCS files have the full history in them?

> 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.

FIrst time I clicked on those links it worked OK but every 
subsequent attempt to access the documents has come up with 
something Acrobat could not process.

Roger

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

Reply via email to