An Hypertextual Electronic Library of Mathematics

(HELM)


Table of contents:

The HELM project [1/1]
Aims [1/2] [2/2]
Application Centric Architecture [1/3] [2/3] [3/3]
Content Centric Architecture [1/5] [2/5] [3/5] [4/5] [5/5]
General Overview [1/1]
The eXtensible Markup Language (XML) [1/4] [2/4] [3/4] [4/4] [example no. 1] [example no. 2]
Encoding CIC in XML: what must NOT be exported from Coq [1/4] [2/4] [3/4] [4/4]
Encoding CIC in XML: terms and objects [1/4] [2/4] [3/4] [4/4]
Encoding CIC in XML: an example of exported object [1/2] [2/2]
Encoding CIC in XML: theories [1/5] [2/5] [3/5] [4/5] [5/5]
Encoding CIC in XML: an example of theory [1/1]
Encoding CIC in XML: cooking and naming [1/5] [2/5] [3/5] [4/5] [5/5] [a cooking example]
A Type Checker for the exported files [1/5] [2/5] [3/5] [4/5] [5/5] [A strange behaviour of Coq]
eXtensible Stylesheet Language Transformations (XSLT) [1/5] [2/5] [3/5] [4/5] [5/5] [An example of XSLT rule]
The Mathematical Markup Language (MathML) [1/5] [2/5] [3/5] [4/5] [5/5] [An example of content markup] [An example of presentation markup]
General overview of the transformations [1/1]
The model of distribution [1/5] [2/5] [3/5] [4/5] [5/5]
Interfaces to the library [1/5] [2/5] [3/5] [4/5] [5/5] [A snapshot of our interface]
 
The exported Standard Library of Coq online