About Mathematical Symbols in Proof General
Currently:
At the moment we suppose that
PGML (or MathML) output is 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
Interesting links/suggestions: