[Axiom-developer] MPL declarative style proofs

[daly]

Very nice. 

I will try to use it as a first example. I've been concentrating
on the ACL2 level at the moment but I just changed Axiom to use
COQ on extracted proofs. Since this works from coqtop it looks like
I can use it for checking during the build.

Thanks for the reference.

Tim