Currently:

- ProofGeneralEmacs relies on X-Symbol
- ProofGeneralKit proposes PGML for simple symbol markup (cf HTML character entities)
- A future possibility is MathML

At the moment we consider PGML (or MathML) output would be produced by the theorem
prover directly in its *output* display.

Since Proof General by design operates on proof scripts in their native language,
there is no provision for generic *input* of mathematical notation. However, with
the ProofGeneralCentralDocumentModel we may provide ways to map from
mathematical notation into prover-input languages. This is the point to
consider connecting to OpenMath
and OMdoc.

TODO: add/discuss future plans here

Topic revision: r1 - 05 Sep 2006 - 14:26:12 - DavidAspinall

Copyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.

Ideas, requests, problems regarding TWiki? Send feedback

This Wiki uses Cookies

Ideas, requests, problems regarding TWiki? Send feedback

This Wiki uses Cookies