Jon,
I had a brief look at the last spec that you posted.
I also had a problem unzipping it, but despite a failure
message got a decompression by opening the file in emacs.
The file decompressed in this way had two issues in it.
The first was that it terminated mid paragraph.
The second was
On Friday 14 Sep 2012 10:36, Phil Clayton wrote:
On 14/09/12 10:05, Roger Bishop Jones wrote:
I had a brief look at the last spec that you posted.
I also had a problem unzipping it, ...
This doesn't surprise me because the attachment was byte
for byte the same as the previous attachment
On 14 Sep 2012, at 03:01, Jon Lockhart wrote:
Phil,
Moving them all to there own paragraph worked great. Now I am up to proving
the consistency of the axioms, which is where I am run into my next stumbling
block. Got the spec load and the consistency goal using the commands no
problem.
Gentlemen,
First, I find it odd that the zipping is not working when before it was for
Phil, and still is for me. I just generated a zip, emailed it to myself,
and then unzipped it and got something that looks just fine, exactly what I
zipped up. I have though created an ascii version of the
On 14/09/12 15:50, Rob Arthan wrote:
When you set up the consistency goal for a Z axiomatic description, what
you see is a mixture of HOL and Z and the existential quantifier is an
HOL quantifier not a Z one. So you would need to use %exists%_tac rather
than z_%exists%_tac. If the axiomatic
On 14/09/12 18:48, Roger Bishop Jones wrote:
(I attach a revised version of your document with the proof
fixed).
In order for z_get_spec to drop the consistency hypothesis, it is
necessary to use save_consistency_thm on the resulting theorem. So
after the proof you need a line like:
Roger,
I see what you did there, and that makes since to me know. That is what I
was trying to achieve, but I was not getting there. Thanks for clearing
that up.
Gentlemen,
Now I have moved on to trying to do the same thing for masterReset, using
the exact same code that Roger has implemented
