XSL Stylesheets for OMDoc

As OMDoc is an XML application, we can use the XSL(T) style sheet language for transforming OMDoc documents into other formats.

We have used style sheets primarily for transforming OMDoc input for presentation (for human consumption) and for machine consumption.

As mathematics heavily relies on notational conventions for symbols and expressions, these style sheets should be augmented by templates that can be generated specifically for the source document to get good results. OMDoc provides a common architecture for this, which we have used in the examples on this page.

Stylesheets for presenting OMDoc Documents to humans

(based on omdoc2share.xsl.

• in HTML, omdoc2html.xsl (uses CSS for styling omdoc-default.css)
• in LaTeX, omdoc2tex.xsl (uses a .sty file omdoc.sty). The BibTeX entry for a document can be extracted by omdoc2bib.xsl (use with care).
• in presentation MathML, omdoc2pmml.xsl (use a MathML-enabled browser like Mozilla to view). The BibTeX entry for a document can be extracted by omdoc2bib.xsl.

Stylesheets for transforming them into machine prover input

• for LambdaClam: omdoc2lclam.xsl
• for the INKA inductive theorem prover omdoc2dgrl.xsl
• for the TPS higher-order theorem prover omdoc2tps.xsl
• for the OMEGA mathematical assistant: omdoc2post.xsl
  • for interfacing with OpenMath components:
    • cd2omdoc.xsl generates OMDoc from OpenMath Content dictionaries.
    • omdoc2cd.xsl generates CDs from OMDocs; use omdoc2defmp.xsl, to generate defmp files

The XML source can be transformed to HTML by the command:

 saxon -o ida.html ida.xml omdoc2html.xsl

This command line produces the HTML document that you can view using Mozilla for the interactivity. Similarly, a LaTeX document can be generated using a different stylesheet:

saxon -o ida.tex ida.xml omdoc2tex.xsl

(Here are the Postscript generated from LaTeX, and the OMDoc).