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 _______________________________________________ Axiom-developer mailing list [email protected] https://lists.nongnu.org/mailman/listinfo/axiom-developer
