About Mathematical Symbols in Proof General


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.

REFACTOR TODO: add/discuss future plans here

Interesting links/suggestions:

This topic: PG > AboutSymbols
Topic revision: r2 - 06 Sep 2006 - 15:26:33 - DavidAspinall
This site is powered by the TWiki collaboration platformCopyright © 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