Proof for Axiom 6.2

[Ian Lynagh]

Hi,

Sorry for the slow reply.

On Fri, Jun 04, 2010 at 03:53:04AM +0200, Thomas Refis wrote:
> Hi!
> I just got the paper-experimental5 repo and ran « make », so I started
> reading theory.pdf and saw that there was no proof for Axiom 6.2 (you
> flaged it as TODO).

Hmm, so it's actually missing not just the proof, but the axiom
statement as well, so it's not being used. Maybe that means the axiom
should be removed.


Incidentally, I can't remember if I've already said this on the list,
but I'm not working on the coq proofs at the moment. Instead, I'm
learning Isabelle, and will possibly be converting the proofs to
Isabelle depending on how that goes.


Thanks
Ian