TWiki> PG Web>AboutSymbols (revision 1)EditAttach

About Mathematical Symbols in Proof General


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.

REFACTOR TODO: add/discuss future plans here

Edit | Attach | Print version | History: r2 < r1 | Backlinks | Raw View | Raw edit | More topic actions...
Topic revision: r1 - 05 Sep 2006 - 14:26:12 - 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