PGML, the Proof General Markup Language
PGML is a simple markup language which was designed for Proof General
to contain elements for describing mathematical symbols (glyphs) as they
appear in the conrete syntax output of proof assistants. The symbol names were
chosen to match the
X-Symbol names which are used by
ProofGeneralEmacs. These in turn are named after TeX and LaTeX macros for generating
symbols.

TODO:
- describe PGML markup
- add list of symbol names
- tools for converting
- relationship to MathML