I'd just like to add that Renaud Rioboo is working on Focal, which seems to be exactly what Cliff Yapp is looking for. However, it is (and will stay) disconnected from Axiom.
As far as I know it is based on Coq and Ocaml. See http://focal.inria.fr/site/manual.html I have no idea in what sense a theorem prover would be useful in a CAS-context. Maybe Bruno Buchberger has some answers: http://www.risc.uni-linz.ac.at/research/theorema/description/ Martin _______________________________________________ Axiom-developer mailing list [email protected] http://lists.nongnu.org/mailman/listinfo/axiom-developer
