Tables (103)

Table p. 28.0 — 7×3, 0 spanning cell(s)
language	MathML	OpenMath
by	W3C Math WG	OpenMath society
origin	math for HTML	integration of CAS
coverage	content + presentation; K14	content; extensible
status	Version 2.2e (VI 2003)	Version 2 (VI 2004)
activity	maintenance	maintenance
Info	http://w3c.org/Math/	http://www.openmath.org/

columns: language | MathML | OpenMath

Table p. 41.1 — 4×2, 0 spanning cell(s)
Level of Representation	OMDoc Example
\begin{tabular}[t]{l} Theory Level: Development Graph \begin{itemize} \item[-] Inheritance via symbol-mapping \item[-] Theory inclusion via proofobligations \item[-] Local (one-step) vs. global links \end{itemize} \end{tabular}	![](https://cdn.mathpix.com/cropped/1b348de5-ed54-4a9a-aba0-06a9a89f7dc6-041.jpg?height=192\&width=504\&top_left_y=539\&top_left_x=762)
\begin{tabular}[t]{l} Statement Level: \begin{itemize} \item[-] Axiom, definition, theorem, proof, example,... \item[-] Structure explicit in statement forms and references \end{itemize} \end{tabular}	\begin{tabular}[t]{l} \begin{itemize} \item[] <definition for="\#plus" type="recursive"> \item[] <CMP>Addition is defined by recursion on the second argument \item[] </CMP> \item[] <FMP> \(X+0=0</ \mathrm{FMP}>\) \item[] \(<\mathrm{FMP}>X+s(Y)=s(X+Y)</ \mathrm{FMP}>\) \end{itemize} \\ </definition> \end{tabular}
\begin{tabular}[t]{l} Object Level: OpenMath/MathML \begin{itemize} \item[-] Objects as logical formulae \item[-] Semantics by pointing to theory level \end{itemize} \end{tabular}	\begin{tabular}[t]{l} \begin{itemize} \item[] <OMA> \item[] <OMS cd="arith1" name="plus"/> \item[] <OMV name="X"/> \item[] <OMS cd="nat" name="zero"/> \end{itemize} \\ </OMA> \end{tabular}

columns: Level of Representation | OMDoc Example

Table p. 50.2 — 2×3, 0 spanning cell(s)
line	Description	ref.
1	This document is an XML 1.0 file that is encoded in the UTF-8 encoding.

columns: line | Description | ref.

Table p. 51.3 — 16×3, 0 spanning cell(s)
2,3	The parser is told to use a document type definition for validation. The string omdoc specifies the name of the root element, the identifier PUBLIC specifies that the DTD (we use the "OMDoc basic" DTD; see Subsection 22.3.1), which can be identified by the public identifier in the first string and looked up in an XML catalog or (if that fails) can be found at the URL specified in the second string. A DTD declaration is not strictly needed for an OMDoc document, but is recommended, since the DTD supplies default values for some attributes.	24.1 p. 228
4	In general, XML files can contain as much whitespace as they want between elements, here we have used it for structuring the document.
5	Start tag of the root element of the document. It declares the version (OMDoc 1.2) via the version, and an identifier of the document using the xml:id attribute. The optional modules specifies the sub-language used in this document. This is used when no DTD is present (see Subsection 22.3.1).	11.1 p. 90
6,7	the namespace prefix declarations for the Dublin Core, Creative Commons, and OpenMath namespaces. They declare the prefixes dc:, cc:, and om:, and bind them to the specified URIs. We will need the OpenMath namespace only in the third markup step described in Section 4.3 but spurious namespace prefix declarations are not a problem in the XML world.	\begin{tabular}[t]{l} 10 \\ 10 p. 83 p. 83 \end{tabular}
8	the namespace declaration for the document; if not prefixed, all elements live in the OMDoc namespace.	10.1 p. 83
9-29	The metadata for the whole document in Dublin Core format	11.2 p. 92
10	The title of the document	12.1 p. 98
11	The document creator, here in the role of a translator	12.2 p. 101
12	The date and time of first creation of the document in ISO 8601 norm format.	12.1 p. 99
13	The date and time of the last update to the document in ISO 8601 norm format.	12.1 p. 99
14-16	A short description of the contents of the document	12.1 p. 99
17-19	Here we acknowledge that the OMDoc document is just a translation from an earlier work.	12.1 p. 100
20	The type of the document, this can be Dataset (un-ordered mathematical knowledge) or Text (arranged for human consumption).	12.1 p. 100
21	The format/MIME type [FB96] of the document, for OMDoc, this is application/omdoc+xml.	12.1 p. 100
22	The copyright resides with the creator of the OMDoc document	12.1 p. 100
23-28	The creator licenses the document to the world under certain conditions as specified in the Creative Commons license specified in this element.	12.3 p. 102

columns: 2,3 | The parser is told to use a document type definition for validation. The string omdoc specifies the name of the root element, the identifier PUBLIC specifies that the DTD (we use the "OMDoc basic" DTD; see Subsection 22.3.1), which can be identified by the public identifier in the first string and looked up in an XML catalog or (if that fails) can be found at the URL specified in the second string. A DTD declaration is not strictly needed for an OMDoc document, but is recommended, since the DTD supplies default values for some attributes. | 24.1 p. 228

Table p. 52.4 — 7×3, 0 spanning cell(s)
24,25	The cc:permissions element gives the world the permission to reproduce and distribute it freely. Furthermore the license grants the public the right to make derivative works under certain conditions.	12.3 p. 103
26	The cc:prohibitions can be used to prohibit certain uses of the document, but this one is unencumbered.	12.3 p. 103
27	The cc:requirements states conditions under which the license is granted. In our case the licensee is required to keep the copyright notice and license notices intact during distribution, to give credit to the copyright holder, and that any derivative works derived from this document must be licensed under the same terms as this document (the copyleft clause).	12.3 p. 103
31-37	The omtext element is used to mark up text fragments. Here, we have simply used a single omtext to classify the whole text in the fragment as unspecific "text".	14.3 p. 124
32-36	The CMP element holds the actual text in a multilingual group. Its xml:lang specifies the language. If the document is used with a DTD or an XML schema (as we are) this attribute is redundant, since the default value given by the DTD or schema is en. More keywords in other languages can be given by adding more CMP elements.	14.1 p. 122
33-35	The text of the \(\mathrm{APT}_{\mathrm{E}} \mathrm{X}\) fragment we are migrating. For simplicity we do not change the text, and leave that to later stages of the migration.
38	The closing tag of the root omdoc element. There may not be text after this in the file.	11.1 p. 90

columns: 24,25 | The cc:permissions element gives the world the permission to reproduce and distribute it freely. Furthermore the license grants the public the right to make derivative works under certain conditions. | 12.3 p. 103

Table p. 53.5 — 7×3, 0 spanning cell(s)
line	Description	ref.
1	The omtext element classifies the text fragment as a definition, other types for mathematical statements include axiom, example, theorem, and lemma. Note that the numbering of the original text is lost, but can be re-created in the text presentation process. The optional xml:id attribute specifies a document-unique identifier that can be used for reference later.	14.3 p. 124
2	A multilingual group of CMP elements that hold the text (in our case, there is only the English default). Here the \(\mathrm{T}_{\mathrm{E}} \mathrm{X}\) formulae have been marked up with legacy elements characterizing them as such. This might simplify a later automatic transformation to OpenMath or Content-MathML.	13.5 p. 120
4-13	We have classified every paragraph in the original as a separate omtext element, which does not carry a type since it does not fit any other mathematical category at the moment.	14.3 p. 124
15	The three examples in the original in Figure 4.1 are grouped into an enumeration. We use the OMDoc omgroup element for this. The optional attribute xml:id can be used for referencing later. We have chosen enumeration for the type attribute to specify the numbering of the examples in the original.	11.4 p. 93
16	We can use the metadata of the omgroup element to accommodate the title "Examples" in the original. We could enter more metadata at this level.	14.1 p. 122
18	The type attribute of this omtext element classifies this text fragment as an example.	14.3 p. 124

columns: line | Description | ref.

Table p. 55.6 — 8×3, 0 spanning cell(s)
line	Description	ref.
1-4	\begin{tabular}[t]{l} The omdoc-basic document type definition is no longer sufficient for our purposes, since we introduce new symbols that can be used in other documents. The DTD for OMDoc content dictionaries (see Chapter 5), which allows this. Correspondingly, we would specify the value cd for the attribute module. \\ The part in line 4 is the internal subset of the DTD, which sets a parameter entity for the modularized DTD to instruct it to accept OpenMath elements in their namespace prefixed form. Of course a suitable namespace prefix declaration is needed as well. \end{tabular}	22.3.2 p. 218
5	The start tag of a theory. We need this, since symbols and definitions can only appear inside theory elements.	15.6 p. 149
6,7	We need to import the theory products to be able to use symbols from it in the definition below. The value of the from is a relative URI reference to a theory element much like the one in line 5. The other imports element imports the theory relation1 from the OpenMath standard content dictionaries \({ }^{1}\). Note that we do not need to import the theory sets here, since this is already imported by the theory products.	15.6.1 p. 150
9-11	A symbol declaration: For every definition, OMDoc requires the declaration of one or more symbol elements for the concept that is to be defined. The name attribute is used to identify it. The dc:description element allows to supply a multilingual (via the xml:lang attribute) group of keywords for the declared symbol	15.2.1 p. 136
12	Upon closer inspection it turns out that the definition in Listing 4.4 actually defines three concepts: "law of composition", "composition", and "magma". Note that "composition" is just another name for the value under the law of composition, therefore we do not need to declare a symbol for this. Thus we only declare one for "law of composition".	15.2.1 p. 136
14	A definition: the definition element carries a name attribute for reference within the theory. We need to reference the two symbols defined here in the for attribute of the definition element; it takes a whitespace-separated list of name attributes of symbol elements in the same theory as values.	15.2.4 p. 139
16	We use an OpenMath object for the set \(E\). It is an om:OMOBJ element with an om:OMV daughter, whose name attribute specifies the object to be a variable with name \(E\). We have chosen to represent the set \(E\) as a variable instead of a constant (via an om:OMS element) in the theory, since it seems to be local to the definition. We will discuss this further in the next section, where we talk about formalization.	13.1.1 p. 108

columns: line | Description | ref.

Table p. 56.7 — 5×3, 0 spanning cell(s)
17-21	This om:0M0BJ represents the Cartesian product \(E \times E\) of the set \(E\) with itself. It is an application (via an om:0MA element) of the symbol for the binary Cartesian product relation to \(E\).	13.1.1 p. 108
18	The symbol for the Cartesian product constructor is represented as an om:0MS element. The cd attribute specifies the theory that defines the symbol, and the name points to the symbol element in it that declares this symbol. The value of the cd attribute is a theory identifier. Note that this theory has to be imported into the current theory, to be legally used.	13.1.1 p. 108
22	We use the term element to characterize the defined terms in the text of the definition. Its role attribute can used to mark the text fragment as a definiens, i.e. a concept that is under definition.	14.5 p. 128
24-28	This object stands for \(f(x, y)\)
30-39	This object represents \((x, y) \in E \times E\). Note that we make use of the symbol for the elementhood relation from the OpenMath core content dictionary set1 and of the pairconstructor from the theory of products from the Bourbaki collection there.

columns: 17-21 | This om:0M0BJ represents the Cartesian product \(E \times E\) of the set \(E\) with itself. It is an application (via an om:0MA element) of the symbol for the binary Cartesian product relation to \(E\). | 13.1.1 p. 108

Table p. 93.8 — 29×4, 17 spanning cell(s) ⚠ overlap at (2,0); overlap at (2,1); overlap at (2,2); overlap at (2,3); overlap at (14,0)
Module	Title	Required?	Chapter
MOBJ	Mathematical Objects	yes	Chapter 13
![](https://cdn.mathpix.com/cropped/1b348de5-ed54-4a9a-aba0-06a9a89f7dc6-093.jpg?height=98\&width=1056\&top_left_y=305\&top_left_x=200)				Formulae are a central part of mathematical documents; this module integrates the content-oriented representation formats OpenMath and MathML into OMDoc
MTXT	Mathematical Text	yes	Chapter 14
Mathematical vernacular, i.e. natural language with embedded formulae
DOC	Document Infrastructure	yes	Chapter 11
A basic infrastructure for assembling pieces of mathematical knowledge into functional documents and referencing their parts
DC	Dublin Core Metadata	yes	Sections 12.1 and 12.2
Contains bibliographical "data about data", which can be used to annotate many OMDoc elements by descriptive and administrative information that facilitates navigation and organization
CC	Creative Commons Metadata	yes	Section 12.3
Licenses for text use
RT	Rich Text Structure	no	Section 14.6
Rich text structure in mathematical vernacular (lists, paragraphs, tables, ...)
ST	Mathematical Statements	no	Chapter 15
![](https://cdn.mathpix.com/cropped/1b348de5-ed54-4a9a-aba0-06a9a89f7dc6-093.jpg?height=132\&width=1061\&top_left_y=980\&top_left_x=200)				Markup for mathematical forms like theorems, axioms, definitions, and examples that can be used to specify or define properties of given mathematical objects and theories to group mathematical statements and provide a notion of context.
PF	Proofs and proof objects	no	Chapter 17
![](https://cdn.mathpix.com/cropped/1b348de5-ed54-4a9a-aba0-06a9a89f7dc6-093.jpg?height=70\&width=1058\&top_left_y=1165\&top_left_x=200)				Structure of proofs and argumentations at various levels of details and formality
ADT	Abstract Data Types	no	Chapter 16
Definition schemata for sets that are built up inductively from constructor symbols
CTH	Complex Theories	no	Chapter 18
Theory morphisms; they can be used to structure mathematical theories
DG	Development Graphs	no	Section 18.5
Infrastructure for managing theory inclusions, change management
EXT	Applets, Code, and Data	no	Chapter 20
Markup for applets, program code, and data (e.g. images, measurements, ...)
PRES	Presentation Information	no	Chapter 19
Limited functionality for specifying presentation and notation information for local typographic conventions that cannot be determined by general principles alone
QUIZ	Infrastructure for Assessments	no	Chapter 21
Markup for exercises integrated into the OMDoc document model

columns: Module | Title | Required? | Chapter

Table p. 94.9 — 6×3, 1 spanning cell(s)
Format	namespace URI	see
Dublin Core	http://purl.org/dc/elements/1.1/ http://creativecommons.org/ns http://www.w3.org/1998/Math/MathML http://www.openmath.org/OpenMath http://www.w3.org/1999/XSL/Transform	Sections 12.1 and 12.2
Section 12.3
MathML		Section 13.2
OpenMath		Section 13.1
XSLT		Chapter 19

columns: Format | namespace URI | see

Table p. 99.10 — 8×5, 2 spanning cell(s)
Element	Attributes		D	Content
Required	Optional	C
omdoc	version， xmlns	xml：id，type，class，style， version，modules	＋	（《top－level》）＊
omgroup	xml：id，modules，type，class， style	＋	（《top－level》）＊
metadata	xml：id，inherits，class，style	－	《（MDelt）＊
ref	xref	type，class，style	－
ignore	type，comment	－	ANY
where 《 top－level》 stands for top－level OMDoc elements，and « \(\langle\) MDelt \(\rangle\) for those introduced in Chapter 12

columns: Element | Attributes Required | Attributes Optional | D C | Content

Table p. 105.11 — 17×4, 2 spanning cell(s)
Element	Attributes
Req．	Optional
dc：creator	xml：id，class，style，role	ANY
dc：contributor	xml：id，class，style，role	ANY
dc：title	xml：lang	《 math vernacular 》
dc：subject	xml：lang	《math vernacular》
dc：description	xml：lang	《 math vernacular 》
dc：publisher	xml：id，class，style	ANY
dc：date	action，who	ISO 8601
dc：type	fixed：＂Dataset＂or＂Text＂
dc：format	fixed：＂application／omdoc＋xml＂
dc：identifier	scheme	ANY
dc：source	ANY
dc：language	ISO 639
dc：relation	ANY
dc：rights	ANY
for 《 math vernacular》 see Section 14.1

columns: Element | Attributes Req． | Attributes Optional | Content

Table p. 111.12 — 6×4, 1 spanning cell(s)
Element	Attributes
Req.	Optional
cc:license	jurisdiction	permissions, prohibitions, requirements
cc:permissions	reproduction, distribution, derivative_works	EMPTY
cc:prohibitions	commercial_use	EMPTY
cc:requirements	notice, copyleft, attribution	EMPTY

columns: Element | Attributes Req. | Attributes Optional | Content

Table p. 111.13 — 4×3, 0 spanning cell(s)
Attribute	Permission	Default
reproduction	the work may be reproduced	permitted
distribution	the work may be distributed, publicly displayed, and publicly performed	permitted
derivative_works	derivative works may be created and reproduced	permitted

columns: Attribute | Permission | Default

Table p. 111.14 — 2×3, 0 spanning cell(s)
Attribute	Prohibition	Default
commercial_use	stating that rights may be exercised for commercial purposes.	permitted

columns: Attribute | Prohibition | Default

Table p. 111.15 — 4×3, 0 spanning cell(s)
Attribute	Requirement	Default
notice	copyright and license notices must be kept intact	required
attribution	credit must be given to copyright holder and/or author	required
copyleft	derivative works, if authorized, must be licensed under the same terms as the work	required

columns: Attribute | Requirement | Default

Table p. 114.16 — 5×4, 1 spanning cell(s)
Element	Attributes		Content
Required	Optional
OMOBJ	id	class, style	See Figure 13.2
m:math	id, xlink:href	See Figure 13.8
legacy	format	xml:id, formalism	\#PCDATA

columns: Element | Attributes Required | Attributes Optional | Content

Table p. 115.17 — 17×4, 2 spanning cell(s)
Element	Attributes		Content
Required	Optional
OMOBJ	id，cdbase，class，style	《（OMel》）？
OMS	cd，name	id，cdbase，class，style	EMPTY
OMV	name	id，class，style	EMPTY
OMA	id，cdbase，class，style	《（OMel》＊
OMBIND	id，cdbase，class，style	《OMel》，OMBVAR，《OMel》
OMBVAR	id，class，style	（OMV｜OMATTR）＋
OMFOREIGN	id，cdbase，class，style	ANY
OMATTR	id，cdbase，class，style	《OMel》
OMATP	id，cdbase，class，style	（OMS，（《OMel》｜OMFOREIGN））＋
OMI	id，class，style	［0－9］＊
OMB	id，class，style	＃PCDATA
OMF	id，class，style，dec，hex	＃PCDATA
OME	id，class，style	《OMel》？
OMR	href	《OMel》？
where 《OMel》 is（OMS｜OMV｜OMI｜OMB｜OMSTR｜OMF｜OMA｜OMBIND｜OME｜OMATTR）

columns: Element | Attributes Required | Attributes Optional | Content

Table p. 120.18 — 2×2, 0 spanning cell(s)
Shared	Exploded
\begin{tabular}[t]{l} \begin{itemize} \item[] <OMOBJ> <OMA> <OMS cd="nat" name="plus" /> <OMA id="t1"> <OMS cd="nat" name="plus" /> <OMA id="t11"> <OMS cd="nat" name="plus" /> <OMI>1</OMI> <OMI>1</OMI> </OMA> <OMR href="\#t11"/> \item[] </OMA> <OMR href="\#t1"/> \item[] </OMA> </OMOBJ> \end{itemize} \end{tabular}	\begin{tabular}[t]{l} \begin{itemize} \item[] <OMOBJ> <OMA> \begin{itemize} \item[] <OMS cd="nat" name="plus" /> <OMA> \begin{itemize} \item[] <OMS cd="nat" name="plus"/> <OMA> \item[] <OMS cd="nat" name="plus"/> <OMI>1</OMI> \item[] <OMI>1</OMI> \item[] </OMA> \item[] <OMA> \item[] <OMS cd="nat" name="plus"/> <OMI>1</OMI> \begin{itemize} \item[] <OMI>1</OMI> \end{itemize} \item[] </OMA> \item[] </OMA> <OMA> \begin{itemize} \item[] <OMS cd="nat" name="plus"/> <OMA> \item[] <OMS cd="nat" name="plus" /> <OMI>1</OMI> <OMI>1</OMI> \item[] </OMA> <OMA> \item[] <OMS cd="nat" name="plus" /> <OMI>1</OMI> <OMI>1</OMI> \item[] </OMA> \item[] </OMA> \end{itemize} \item[] </OMA> \end{itemize} \item[] </OMOBJ> \end{itemize} \end{itemize} \end{tabular}

columns: Shared | Exploded

Table p. 121.19 — 1×2, 0 spanning cell(s)
\begin{itemize} \item[] <OMOBJ> \begin{itemize} \item[] <OMA id="bar"> \begin{itemize} \item[] <OMS cd="nat" name="plus" /> \item[] <OMI>1</OMI> \item[] <OMR href="\#baz"/> \end{itemize} \item[] </OMA> \end{itemize} \item[] </OMOBJ> \end{itemize}	\begin{itemize} \item[] <OMOBJ> \begin{itemize} \item[] <OMA id="baz"> \begin{itemize} \item[] <OMS cd="nat" name="plus" /> \item[] <OMI>1</OMI> \item[] <OMR href="\#bar"/> \item[] </OMA> \end{itemize} \end{itemize} \item[] </OMOBJ> \end{itemize}

columns: \begin{itemize} \item[] <OMOBJ> \begin{itemize} \item[] <OMA id="bar"> \begin{itemize} \item[] <OMS cd="nat" name="plus" /> \item[] <OMI>1</OMI> \item[] <OMR href="\#baz"/> \end{itemize} \item[] </OMA> \end{itemize} \item[] </OMOBJ> \end{itemize} | \begin{itemize} \item[] <OMOBJ> \begin{itemize} \item[] <OMA id="baz"> \begin{itemize} \item[] <OMS cd="nat" name="plus" /> \item[] <OMI>1</OMI> \item[] <OMR href="\#bar"/> \item[] </OMA> \end{itemize} \end{itemize} \item[] </OMOBJ> \end{itemize}

Table p. 122.20 — 12×4, 1 spanning cell(s)
Element	Attributes	Content
Required	Optional
m：math	id，xlink：href	《CMel》＋
m：apply	id，xlink：href	m：bvar？，《 CMel》＊
m：csymbol	definitionURL	id，xlink：href	m：EMPTY
m：ci	id，xlink：href	＃PCDATA
m：cn	id，xlink：href	（［0－9］｜，｜．）（＊｜e（［0－9］｜，｜．）＊）？
m：bvar	id，xlink：href	m：ci｜m：semantics
m：semantics	id，xlink：href， definitionURL	《CMel》，（m：annotation｜ m：annotation－xml）＊
m：annotation	definitionURL， encoding	＃PCDATA
m：annotation－xml	definitionURL， encoding	ANY
where 《CMel》 is m：apply｜m：csymbol｜m：ci｜m：cn｜m：semantics

columns: Element | Attributes | | Content

Table p. 128.21 — 9×5, 1 spanning cell(s)
Element	Attributes		D	Content
Required	Optional	C
CMP	xml：lang，id	－	《math vernacular》
FMP	xml：id，logic	－	（assumption＊，conclusion＊）｜ OMOBJ｜m：math｜legacy
assumption	xml：id，inductive， class，style	＋	（OMOBJ｜m：math｜legacy）
conclusion	xml：id，class，style	＋	（OMOBJ｜m：math｜legacy）
phrase	xml：id，class，style， index，verbalizes， type	－	《math vernacular》
term	cd，name	role，xml：id，class， style	－	《math vernacular》
omtext	xml：id，type， for，class，style， verbalizes	＋	CMP＋，FMP＊

columns: Element | Attributes Required | Attributes Optional | D C | Content

Table p. 129.22 — 6×4, 0 spanning cell(s)
Module	Elements	Comment	see
MOBJ	om:0M0BJ, m:math, legacy	mathematical Objects	p. 107
MTXT	phrase, term	phrase-level markup	below
DOC	ref, ignore	document structure	p. 89
RT	p, ol, ul, dl, table, link, note, idx	rich text structure	p. 128
EXT	omlet	for applets, images, ...	p. 205

columns: Module | Elements | Comment | see

Table p. 136.23 — 19×4, 0 spanning cell(s)
Element	Optional Attributes	DC	Content
p	xml：id，style，class，index，verbalizes	＋	《math vernacular》
ol	xml：id，style，class，index，verbalizes	＋	li＊
ul	xml：id，style，class，index，verbalizes	＋	li＊
li	xml：id，style，class，index，verbalizes	＋	《math vernacular》
dl	xml：id，style，class，index，verbalizes	＋	di＊
di	xml：id，style，class，index，verbalizes	＋	dt＊，dd＊
dt	xml：id，style，class，index，verbalizes	＋	《math vernacular》
dd	xml：id，style，class，index，verbalizes	＋	《math vernacular》
idx	（xml：id｜xref）	－	idt？，ide＋
ide	index，sort－by，see，seealso，links	－	idp＊
idt	style，class	－	《math vernacular》
idp	sort－by，see，seealso，links	－	《math vernacular》
table	xml：id，style，class，index，verbalizes	＋	tr＊
tr	xml：id，style，class，index，verbalizes	＋	td＊
td	xml：id，style，class，index，verbalizes	＋	《math vernacular》
th	xml：id，style，class，index，verbalizes	＋	《math vernacular》
link	xml：id，style，class，index，verbalizes	－	《math vernacular》
note	type，xml：id，style，class，index，verbalizes	＋	《math vernacular》

columns: Element | Optional Attributes | DC | Content

Table p. 141.24 — 4×3, 0 spanning cell(s)
Definiendum	Definiens	Type
The number 1	\(1:=s(0)\) (1 is the successor of 0)	simple
The exponential function \(e^{\cdot}\)	The exponential function \(e\) is the solution to the differential equation \(\partial f=f[\) where \(f(0)=1]\).	implicit
The addition function +	Addition on the natural numbers is defined by the equations \(x+0=x\) and \(x+s(y)=s(x+y)\).	recursive

columns: Definiendum | Definiens | Type

Table p. 142.25 — 10×5, 2 spanning cell(s)
Element	Attributes		D	Content
Required	Optional	C
symbol	name	xml：id，role，scope，style， class	＋	type＊
type	xml：id，system，style， class	－	CMP＊，\(\langle\langle\) mobj \(\rangle\rangle\)
axiom	xml：id，for，type，style， class	＋	CMP＊，FMP＊
definition	for	xml：id，type，style，class， uniqueness，existence， consistency，exhaustivity	＋	CMP＊，（FMP＊｜requation＋｜《（mobj》）？，measure？， ordering？
requation	xml：id，style，class	－	《 \(\langle\) mobj \(\rangle\) ，《 \(\langle\) mobj \(\rangle\)
measure	xml：id，style，class	－	《（mobj》
ordering	xml：id，style，class	－	《（mobj》）
where 《 mobj》 is（OMOBJ｜m：math｜legacy）

columns: Element | Attributes Required | Attributes Optional | D C | Content

Table p. 148.26 — 7×5, 2 spanning cell(s)
Element	Attributes		D	Content
Required	Optional	C
assertion	xml：id，for，type， theory，class，style， status，just－by	＋	CMP＊，FMP＊
type	system	xml：id，for，just－by， theory，class，style	－	CMP＊，《 \(\langle\) mobj \(\rangle\) ，〈 \(\langle\) mobj \(\rangle\) 〉
example	for	xml：id，type， assertion，theory， class，style	＋	CMP＊｜\(\langle\langle\) mobj \(\rangle\rangle *\)
alternative	for，theory， entailed－by， entails， entailed－by－thm， entails－thm	xml：id，type，theory， class，style	＋	CMP＊，（FMP＊｜ requation＊｜《（mobj》））
where 《 mobj》 is（OMOBJ｜m：math｜legacy）

columns: Element | Attributes Required | Attributes Optional | D C | Content

Table p. 149.27 — 15×2, 7 spanning cell(s)
Value	Explanation
theorem, proposition	an important assertion with a proof
Note that the meaning of the type (in this case the existence of a proof) is not enforced by OMDoc applications. It can be appropriate to give an assertion the type theorem, if the author knows of a proof (e.g. in the literature), but has not formalized it in OMDoc yet.
lemma	a less important assertion with a proof
The difference of importance specified in this type is even softer than the other ones, since e.g. reusing a mathematical paper as a chapter in a larger monograph, may make it necessary to downgrade a theorem (e.g. the main theorem of the paper) and give it the status of a lemma in the overall work.
corollary	a simple consequence
An assertion is sometimes marked as a corollary to some other statement, if the proof is considered simple. This is often the case for important theorems that are simple to get from technical lemmata.
postulate, conjecture	an assertion without proof or counter-example
Conjectures are assertions, whose semantic value is not yet decided, but which the author considers likely to be true. In particular, there is no proof or counterexample (see Section 15.4).
false-conjecture	an assertion with a counter-example
A conjecture that has proven to be false, i.e. it has a counter-example. Such assertions are often kept for illustration and historical purposes.
obligation, assumption	an assertion on which the proof of another depends
These kinds of assertions are convenient during the exploration of a mathematical theory. They can be used and proven later (or assumed as an axiom).
formula	if everything else fails
This type is the catch-all if none of the others applies.

columns: Value | Explanation

Table p. 150.28 — 26×2, 13 spanning cell(s)
status	just-by points to
tautology	Proof of \(\mathcal{F}\)
All \(\mathcal{T}\)-interpretations satisfy \(\mathcal{A}\) and some \(\mathcal{C}_{i}\)
tautologous-conclusion	Proof of \(\mathcal{F}_{c}\).
All \(\mathcal{T}\)-interpretations satisfy some \(\mathcal{C}_{j}\)
equivalent	Proofs of \(\mathcal{F}\) and \(\mathcal{F}^{-1}\)
\(\mathcal{A}\) and \(\mathcal{C}\) have the same \(\mathcal{T}\)-models (and there are some)
theorem	Proof of \(\mathcal{F}\)
All \(\mathcal{T}\)-models of \(\mathcal{A}\) (and there are some) satisfy some \(\mathcal{C}_{i}\)
satisfiable	Model of \(\mathcal{A}\) and some \(\mathcal{C}_{i}\)
Some \(\mathcal{T}\)-models of \(\mathcal{A}\) (and there are some) satisfy some \(\mathcal{C}_{i}\)
contradictory-axioms	Refutation of \(\mathcal{A}\)
There are no \(\mathcal{T}\)-models of \(\mathcal{A}\)
no-consequence	\(\mathcal{T}\)-model of \(\mathcal{A}\) and some \(\mathcal{C}_{i}, \mathcal{T}\)-model of \(\mathcal{A} \cup \overline{\mathcal{C}}\).
Some \(\mathcal{T}\)-models of \(\mathcal{A}\) (and there are some) satisfy some \(\mathcal{C}_{i}\), some satisfy \(\overline{\mathcal{C}}\)
counter-satisfiable	Model of \(\mathcal{A} \cup \overline{\mathcal{C}}\)
Some \(\mathcal{T}\)-models of \(\mathcal{A}\) (and there are some) satisfy \(\overline{\mathcal{C}}\)
counter-theorem	Proof of \(\overline{\mathcal{C}}\) from \(\mathcal{A}\)
All \(\mathcal{T}\)-models of \(\mathcal{A}\) (and there are some) satisfy \(\overline{\mathcal{C}}\)
counter-equivalent	Proof of \(\overline{\mathcal{C}}\) from \(\mathcal{A}\) and proof of \(\mathcal{A}\) from \(\overline{\mathcal{C}}\)
\(\mathcal{A}\) and \(\overline{\mathcal{C}}\) have the same \(\mathcal{T}\)-models (and there are some)
unsatisfiable-conclusion	Proof of \(\overline{\mathcal{C}}\)
All \(\mathcal{T}\)-interpretations satisfy \(\overline{\mathcal{C}}\)
unsatisfiable	Proof of \(\neg \mathcal{F}\)
All \(\mathcal{T}\)-interpretations satisfy \(\mathcal{A}\) and \(\overline{\mathcal{C}}\)
Where \(\mathcal{F}\) is an assertion whose FMP has assumption elements \(\mathcal{A}_{1}, \ldots, \mathcal{A}_{n}\) and conclusion elements \(\mathcal{C}_{1}, \ldots, \mathcal{C}_{m}\). Furthermore, let \(\mathcal{A}:=\left\{\mathcal{A}_{1}, \ldots, \mathcal{A}_{n}\right\}\) and \(\mathcal{C}:=\left\{\mathcal{C}_{1}, \ldots, \mathcal{C}_{m}\right\}\), and \(\mathcal{F}^{-1}\) be the sequent that has the \(\mathcal{C}_{i}\) as assumptions and the \(\mathcal{A}_{i}\) as conclusions. Finally, let \(\overline{\mathcal{C}}:=\left\{\overline{\mathcal{C}_{1}}, \ldots, \overline{\mathcal{C}_{m}}\right\}\), where \(\overline{\mathcal{C}_{i}}\) is a negation of \(\mathcal{C}_{i}\).

columns: status | just-by points to

Table p. 156.29 — 6×5, 2 spanning cell(s)
Element	Attributes		D
Req．	Optional	C
theory	xml：id，class，style，cdbase，cdversion， cdrevision，cdstatus，cdurl，cdreviewdate	＋	（《top＋thc》｜ imports）＊
imports	from	id，type，class，style	＋
tgroup	xml：id，modules，type，class，style	＋	\((\langle\langle t o p+t h c\rangle\rangle) *\)
where 《 top＋thc》 stands for top－level and theory－constitutive elements

columns: Element | Attributes Req． | Attributes Optional | D C | Content

Table p. 162.30 — 9×5, 1 spanning cell(s)
Element	Attributes		D	Content
Req．	Optional	C
adt	xml：id，class，style， parameters	＋	sortdef＋
sortdef	name	type，role，scope，class， style	＋	（constructor｜ insort）＊，recognizer？
constructor	name	type，scope，class，style	＋	argument＊
argument	＋	type，selector？
insort	for	－
selector	name	type，scope，role，total， class，style	＋	EMPTY
recognizer	name	type，scope，role，class， style	＋

columns: Element | Attributes Req． | Attributes Optional | D C | Content

Table p. 168.31 — 8×5, 1 spanning cell(s)
Element	Attributes		D	Content
Req.	Optional	C
proof	for	theory, xml:id, class, style	+	(omtext \| derive \| hypothesis \| symbol \| definition)*
proofobject	xml:id, for, class, style, theory	+	CMP*, (OMOBJ \|m:math \|legacy)
hypothesis	xml:id, class, style, inductive	-	CMP, FMP
derive	xml:id, class, style, type	-	CMP, FMP, method?
method	xref	-	(OMOBJ \|m:math \|legacy \| premise \| proof \| proofobject)*
premise	xref	-	EMPTY

columns: Element | Attributes Req. | Attributes Optional | D C | Content

Table p. 178.32 — 8×5, 1 spanning cell(s)
Element	Attributes		D	Content
Required	Optional	C
theory	xml:id, class, style	+	(《top-level》\| imports \| inclusion)*
imports	from	xml:id, type, class, style, conservativity, conservativity-just	+	morphism?
morphism	xml:id, base, class, style, type, hiding, consistency, exhaustivity	-	requation*, measure?, ordering?
inclusion	via	xml:id, conservativity, conservativity-just	-	EMPTY
theory-inclusion	from, to	xml:id, class, style, conservativity, conservativity-just	+	(CMP,FMP, morphism, obligation*)
axiom-inclusion	from, to	xml:id, class, style, conservativity, conservativity-just	+	morphism?, obligation*

columns: Element | Attributes Required | Attributes Optional | D C | Content

Table p. 189.33 — 6×5, 1 spanning cell(s)
Element	Attributes		D	Content
Required	Optional	C
decomposition	links	-	EMPTY
path-just	local, globals	for	-	EMPTY
theory-inclusion	from, to, by	xml:id, class, style	+	(CMP,FMP, morphism, (decomposition* \| obligation*))
axiom-inclusion	from, to	xml:id, class, style	+	morphism?, (path-just* \| obligation*)

columns: Element | Attributes Required | Attributes Optional | D C | Content

Table p. 192.34 — 6×4, 1 spanning cell(s)
Element	Attributes		Content
Required	Optional
omstyle	element	for, xml:id, xref, class, style	(style\|xslt)*
presentation	for	xml:id, xref, fixity, role, lbrack, rbrack, separator, bracket-style, class, style, precedence, crossref-symbol	(use \| xslt \| style)*
xslt	format	xml:lang, requires, xref	XSLT fragment
use	format	xml:lang, requires, fixity, lbrack, rbrack, separator, element, attributes, crossref-symbol	(element \| text \| recurse \| map \| value-of)*

columns: Element | Attributes Required | Attributes Optional | Content

Table p. 195.35 — 10×4, 0 spanning cell(s)
Element	Attributes	Content
Required	Optional
style	format	xml:lang, requires, xref	(element \| text \| recurse \| map \| value-of)*
element	name	crid, cr, ns	(attribute \| element \| text \| value-of \| recurse \| map)*
attribute	name	(value-of \| text)*
text	(\#PCDATA)
value-of	select	EMPTY
recurse	select	EMPTY
map	select	separator?, (element \| text \| recurse \| map)
separator	(element \| text \| recurse \| map)

columns: Element | Attributes | | Content

Table p. 201.36 — 7×3, 0 spanning cell(s)
Precedence	Operators	Comment
200	+,-	unary
200	-	exponentiation
400	\(*, \wedge, \cap\)	multiplicative
500	+, -, V, U	additive
600	/	fraction
700	\(=, \neq, \leq,<,>, \geq\)	relation

columns: Precedence | Operators | Comment

Table p. 201.37 — 6×4, 1 spanning cell(s)
fixity	bracket-style	separator	yields
prefix	lisp	" "	(f123)
postfix	lisp	" "	(123f)
prefix	math	","	f(1, 2, 3)
postfix	math	","	(1,2,3)f
assuming lbrack="(" and rbrack=")"

columns: fixity | bracket-style | separator | yields

Table p. 202.38 — 3×2, 1 spanning cell(s)
Notation specification	Example
\begin{lstlisting}[mathescape=true] <presentation for=" #forall" role="binding" separator = ". " \(>\) <use format="TeX"> forall</use> <use format="html">∀</use> </presentation> \end{lstlisting}	\begin{lstlisting}[mathescape=true] <OMBIND> <OMS cd="quant1" name="forall"/> <OMBVAR> <OMV name="X"/> </OMBVAR> <OMS cd="logic1" name="true"/> </OMBIND> \end{lstlisting}
\begin{tabular}[t]{l} Using XSLT templates induced from the presentation element on the OpenMath expression yields \(\forall X\).true, where the glyph \(\forall\) carries a hyperlink \({ }^{\varnothing}\) to it definition, as the crossref-symbol on the presentation element has the default value yes. Internally, the hyperlinks are format-dependent, we have: \\ LATEX: \begin{lstlisting} \href{../ocd/logic1.ps#true}{\forall}X. \href{../ocd/logic1.ps#true}{{\sf true}} HTML: <a href="../ocd/logic1.html#forall">∀</a> X. <a href="../ocd/logic1.html#true"><b>true</b></a> \end{lstlisting} \end{tabular}

columns: Notation specification | Example

Table p. 206.39 — 8×5, 1 spanning cell(s)
Element	Attributes		D
Req.	Optional	C
private	xml:id, for, theory, requires, type, reformulates, class, style	+	CMP*, data+
code	xml:id, for, theory, requires, type, class, style	+	CMP*, input?, output?, effect?, data+
input	xml:id, style, class	+	CMP, FMP
output	xml:id, style, class	+	CMP, FMP
effect	xml:id, style, class	+	CMP, FMP
data	format, href, size, original, pto, pto-version	-	<![CDATA[...]]>

columns: Element | Attributes Req. | Attributes Optional | D C | Content

Table p. 210.40 — 4×5, 1 spanning cell(s)
Element	Attributes		D	Content
Req.	Optional	C
omlet	data,	xml:id, action, show, actuate, class, style	+	(《CMP content》 \| param),data
param	name	value, valuetype	-	EMPTY

columns: Element | Attributes Req. | Attributes Optional | D C | Content

Table p. 214.41 — 8×5, 1 spanning cell(s)
Element	Attributes		D	Content
Req.	Optional	C
exercise	xml:id, class, style	+	CMP,FMP,hint?,(solution\|mc)
hint	xml:id, class, style	+	CMP, FMP
solution	xml:id, for, class, style	+	《top-level element》
mc	xml:id, for, class, style	-	choice, hint?, answer
choice	xml:id, class, style	+	CMP, FMP
answer	verdict	xml:id, class, style	+	CMP, FMP

columns: Element | Attributes Req. | Attributes Optional | D C | Content

Table p. 220.42 — 5×4, 0 spanning cell(s)
\#	Rule	comment	elements
1	unordere d	The order of children of this element is irrelevant (as far as permitted by the content model). For instance only the order of obligation elements in the axiom-inclusion element is arbitrary, since the others must precede them in the content model.	adt axiom-inclusion metadata symbol code private presentation omstyle
2	multigroup	The order between siblings elements does not matter, as long as the values of the key attributes differ.	CMP FMP requation dc:description sortdef data dc:title solution
3	DAG encoding	Directed acyclic graphs built up using om:OMR elements are equal, iff their tree expansions are equal.	om:OMR ref
4	Dataset	If the content of the dc:type element is Dataset, then the order of the siblings of the parent metadata element is irrelevant.	dc:type

columns: \# | Rule | comment | elements

Table p. 227.43 — 7×2, 0 spanning cell(s)
directories	content
bin, lib, oz, thirdParty	programs and third-party software used in the administration and examples
css, xsl	style sheets for displaying OMDoc documents on the web, see Chapter 25 for a discussion.
doc	The OMDoc documentation, including the specification, papers about a the OMDoc format and tools.
dtd, rnc	The OMDoc document type definition and the RelaxNG schemata for OMDoc
examples	Various example documents in OMDoc format.
projects	various contributed developments for OMDoc. Documentation is usually in their doc sub-directory

columns: directories | content

Table p. 233.44 — 7×3, 0 spanning cell(s)
language	namespace	prefix
MathML	http://www.w3.org/1998/Math/MathML	m:
OpenMath	http://www.openmath.org/OpenMath	om:
XSLT	http://www.w3.org/1999/XSL/Transform	xsl:
Dublin Core	http://purl.org/dc/elements/1.1/	dc:
Creative Commons	http://creativecommons.org/ns	cc:
OMDoc	http://www.mathweb.org/omdoc	omdoc:

columns: language | namespace | prefix

Table p. 245.45 — 2×2, 0 spanning cell(s)
Project Home	http://www.matracas.org/qmath/index.en.html
Authors	Alberto González Palomo Toledo, Spain \({ }^{2}\)

columns: Project Home | http://www.matracas.org/qmath/index.en.html

Table p. 248.46 — 2×2, 0 spanning cell(s)
Project Home	http://www.matracas.org/sentido/index.en.html
Authors	Alberto González Palomo Toledo, Spain \({ }^{4}\)

columns: Project Home | http://www.matracas.org/sentido/index.en.html

Table p. 253.47 — 2×2, 0 spanning cell(s)
Project Home	http://www.mathweb.org/mbase
Authors	Andreas Franke \({ }^{1}\), Michael Kohlhase \({ }^{2}\) \begin{itemize} \item[] \({ }^{1}\) Computer Science, Saarland University \item[] \({ }^{2}\) School of Engineering and Science, International \end{itemize} University Bremen

columns: Project Home | http://www.mathweb.org/mbase

Table p. 255.48 — 2×2, 0 spanning cell(s)
Project Home	http://search.mathweb.org/
Authors	Ioan Sucan, Michael Kohlhase Computer Science, International University Bremen

columns: Project Home | http://search.mathweb.org/

Table p. 259.49 — 2×2, 0 spanning cell(s)
Project Home	http://www.mmiss.de
Authors	Bernd Krieg-Brückner, Achim Mahnke Computer Science, University of Bremen, Germany

columns: Project Home | http://www.mmiss.de

Table p. 263.50 — 2×2, 0 spanning cell(s)
Project Home	http://www.mathdox.org
Authors	A.M. Cohen, H. Cuypers, E. Reinaldo Barreiro Department of Mathematics and Computer Science, Eindhoven University of Technology

columns: Project Home | http://www.mathdox.org

Table p. 267.51 — 2×2, 0 spanning cell(s)
Project Home	http://www.activemath.org/
Authors	The ActiveMath group: Erica Melis, Giorgi Goguadse, Alberto Gonzales-Palomo, Adrian Frischauf, Martin Homik, Paul Libbrecht, Carsten Ullrich DFKI GmbH and Universität des Saarlandes

columns: Project Home | http://www.activemath.org/

Table p. 273.52 — 2×2, 0 spanning cell(s)
Project Home	http://www.activemath.org/projects/jEdit0QMath
Authors	Paul Libbrecht DFKI GmbH and Universität des Saarlandes

columns: Project Home | http://www.activemath.org/projects/jEdit0QMath

Table p. 275.53 — 2×2, 0 spanning cell(s)
Project Home	http://kwarc.eecs.iu-bremen.de/projects/swim
Authors	Christoph Lange, Michael Kohlhase Computer Science, International University Bremen

columns: Project Home | http://kwarc.eecs.iu-bremen.de/projects/swim

Table p. 279.54 — 2×2, 0 spanning cell(s)
Project Home	http://www.cs.nott.ac.uk/ \({ }^{\sim}\) lad/research/ challenges/challenge_manager.html
Authors	Thomas D. Attfield, Monica C. Duarte, Lin Li, HoYing Mak, Adam M. Neal, Lewis M. Toft, Zixuan Wang, Louise A. Dennis School of Computer Science and Information Technology, University of Nottingham

columns: Project Home | http://www.cs.nott.ac.uk/ \({ }^{\sim}\) lad/research/ challenges/challenge_manager.html

Table p. 282.55 — 2×2, 0 spanning cell(s)
Project Home	www.dfki.de/ \({ }^{\sim}\) inka/maya.html
Authors	Serge Autexier \({ }^{1}\), Dieter Hutter \({ }^{1}\), Till Mossakowski \({ }^{2}\), Axel Schairer \({ }^{1} { }^{1}\) DKFI GmbH, Stuhlsatzenhausweg 3, D 66123 Saarbrücken \({ }^{2}\) Computer Science, University of Bremen, Germany

columns: Project Home | www.dfki.de/ \({ }^{\sim}\) inka/maya.html

Table p. 287.56 — 2×2, 0 spanning cell(s)
Project Home	www.tzi.de/cofi/hets
Authors	Till Mossakowski, Christian Maeder, Klaus Lüttich Computer Science, University of Bremen, Germany

columns: Project Home | www.tzi.de/cofi/hets

Table p. 291.57 — 2×2, 0 spanning cell(s)
Project Home	http://kwarc.eecs.iu-bremen.de/software/CPoint/
Authors	\begin{tabular}[t]{l} Andrea Kohlhase \\ Digital Media in Education (DiMeB), Dept. of Mathematics and Computer Science, University Bremen \end{tabular}

columns: Project Home | http://kwarc.eecs.iu-bremen.de/software/CPoint/

Table p. 295.58 — 2×2, 0 spanning cell(s)
Project Home	http://kwarc.iu-bremen.de/projects/stex/
Authors	Michael Kohlhase Computer Science, International University Bremen

columns: Project Home | http://kwarc.iu-bremen.de/projects/stex/

Table p. 299.59 — 2×2, 0 spanning cell(s)
Project Home	http://www.cs.cmu.edu/ \({ }^{\sim}\) ccaps
Authors	Peter Jansen School of Computer Science, Carnegie Mellon University

columns: Project Home | http://www.cs.cmu.edu/ \({ }^{\sim}\) ccaps

Table p. 302.60 — 2×2, 0 spanning cell(s)
Project Home	http://www.cs.cmu.edu/ \({ }^{\sim}\) ccaps
Authors	Klaus Sutner School of Computer Science, Carnegie Mellon University

columns: Project Home | http://www.cs.cmu.edu/ \({ }^{\sim}\) ccaps

Table p. 305.61 — 2×2, 0 spanning cell(s)
Project Home	http://www.mathweb.org/omdoc/examples/logics
Authors	Michael Kohlhase Computer Science, International University Bremen

columns: Project Home | http://www.mathweb.org/omdoc/examples/logics

Table p. 306.62 — 14×4, 0 spanning cell(s)
PVS	\(\Omega\) MEGA	PVS	\(\Omega_{\text {MEGA }}\)
set	subset?	subset
member	in	subset2
empty?	empty	strict_subset?	proper-subset
emptyset	emptyset	superset
nonempty?	not-empty	union	union
full?	union2
fullset	union-over-collection
singleton?	singleton	intersection	intersection
singleton	intersection-over-coll.
complement	set-complement	disjoint?	misses
difference	setminus	meets
symmetric_difference	add	add-one
exclunion	remove

columns: PVS | \(\Omega\) MEGA | PVS | \(\Omega_{\text {MEGA }}\)

Table p. 310.63 — 2×2, 0 spanning cell(s)
Project Home	http://www.ags.uni-sb.de/~omega/projects/ verimathdoc
Authors	Serge Autexier, Christoph Benzmüller, Armin Fiedler, and Henri Lesourd Computer Science, Saarland University, Saarbrücken, Germany

columns: Project Home | http://www.ags.uni-sb.de/~omega/projects/ verimathdoc

Table p. 314.64 — 2×2, 0 spanning cell(s)
Project Home	http://www.verifun.de/
Authors	Normen Müller School of Engineering and Science, International University Bremen

columns: Project Home | http://www.verifun.de/

Table p. 320.65 — 4×4, 0 spanning cell(s)
element	state	comments	cf.
alternative	aug	This element can now have theory, generated-from, and generated-via attributes.	145
argument	cha	The sort has been replaced by a type child, so that higher-order sorts can be specified.	156
assertion	aug	the assertion element now has an optional for attribute. Furthermore, an optional attribute generated-via has been added to allow generation via a theory morphism. Finally, two new attributes status and just-by have been added to mark up the deductive status of the assertion.	142

columns: element | state | comments | cf.

Table p. 321.66 — 10×4, 0 spanning cell(s)
assumption	cha	This element can now have an attribute inductive for inductive assumptions. The natural langauge description in the optional CMP element is no longer allowed, use a phrase element in a CMP that is a sibling to the FMP instead.	145
adt	aug	the adt loses the CMP and commonname children, use the Dublin Core metadata elements dc:description and dc:subject instead. The type attribute is now on the sortdef element. Furthermore, an optionala attribute generated-via has been added to allow generation via a theory morphism. Finally, an attribute parameters has been added to allow for parametric ADTs.	156
answer	cha	the answer element does not allow symbol children any more, if these are needed, the exercise should have its own theory.	210
attribute	aug	the attribute element now has a optional ns attribute for the namespace URI of the generated attribute node and an attribute select for an XPath expression that specifies the value of the generated attribute.	191
axiom	aug	the axiom element now has an optional for attribute which can point to a list of symbols. Furthermore, an optional attribute generated-via has been added to allow generation via a theory morphism and an attribute type is now also allowed.	138
axiom-inclusion	lib	the axiom-inclusion element can now contain multiple path-just children to record multiple justifications. Furthermore, it can now have theory, generated-from, and generated-via attributes. New optional attributes conservativity and conservativity-just for stating and justifying conservativity.	180
catalogue	dep	the catalogue mechanism has been eliminated.
choice	cha	the choice element does not allow symbol children any more, if these are needed, the exercise should have its own theory	210
code	cha	Attributes classid and codebase are deprecated. The attributes pto and pto-version have moved to the data element. The attribute type has been removed and optional attributes theory, generated-from, and generated-via have been added.	202
commonname	dep	This element is deprecated in favor of a metadata/dc:subject element.

columns: assumption | cha | This element can now have an attribute inductive for inductive assumptions. The natural langauge description in the optional CMP element is no longer allowed, use a phrase element in a CMP that is a sibling to the FMP instead. | 145

Table p. 322.67 — 11×4, 0 spanning cell(s)
conclusion	cha	The natural langauge description in the optional CMP element is no longer allowed, use a phrase element in a CMP that is a sibling to the FMP instead.	124
constructor	cha	The role attribute is now fixed to object. The commonname child has been replaced by an initial metadata element.	156
data	aug	new optional attributes original to specify whether the external resource referenced by the href attribute (value external) or the data content is the original (value local). The data element has acquired attributes pto and pto-version from the code and private elements.	203
dc:*	aug	All Dublin Core tags have been lowercased to synchronize with the tag syntax recommended by the Dublin Core Initiative. The tags were capitalized in OMDoc1.1. Furthermore, dc:contributor, dc:creator, dc:publisher have received an optional xml:id attribute, so that they can be crossreferenced by the new who of the dc : date element.	98
decomposition	aug	The for attribute is now optional, it need not be given, if the element is a child of a theory-inclusion element. Furthermore, it can now have a theory, generated-from, and generated-via attributes.	184
dc:description	aug	The dc:description can now have the optional xml:id, and CSS attributes	99
definition	aug	The definition element can now have the type pattern for pattern-defined functions. This is a degenerate case of the type inductive. Furthermore, an optional attribute generated-via has been added to allow generation via a theory morphism.	139
effect	aug	allows an optional xml:id attribute	204
example	aug	The example element now has the optional theory attribute that specifies the home theory. Furthermore, it can now have attributes theory, generated-from, and generated-via.	146
exercise	cha	the exercise element does not allow symbol children any more, if these are needed, the exercise should have its own theory. Furthermore, it can now have a theory, generated-from, and generated-via attributes.	209
extradata	cha	The content of the old extradata element can now be directly in the metadata/dc:subject element.

columns: conclusion | cha | The natural langauge description in the optional CMP element is no longer allowed, use a phrase element in a CMP that is a sibling to the FMP instead. | 124

Table p. 323.68 — 13×4, 0 spanning cell(s)
element	aug	The element element now allows the map and separator elements in the body. Furthermore, it carries the optional attributes crid for parallel markup, cr for cross-references, and ns for specifying the namespace.	190
hint	aug	the hint element can now appear on toplevel and has a for attribute. It does not allow symbol children any more, if these are needed, the exercise should have its own theory. Furthermore, the exercise can now have a theory, generated-from, and generated-via attributes.	209
hypothesis	cha	the discharged-in attribute has been eliminated. Scoping is now specified in terms of the enclosing proof element. Furthermore, the symbol child is no longer allowed inside the element. A sibling symbol should be used.	162
inclusion	aug	allows optional attributes xml:id, conservativity, and conservativity-just for stating and justifying conservativity.	179
imports	lib	the xml:id is now optional. New optional attributes conservativity and conservativity-just for stating and justifying conservativity.	150
input	aug	allows an optional xml:id attribute	204
legacy	new	An element for encapsulating legacy mathematics, can be used wherever m:math and om:OMOBJ are allowed.	120
loc	dep	The catalogue mechanism has been eliminated.
m:math	new	Content-MathML is now allowed wherever OpenMath objects were allowed before.	114
map	new	this element allows to map its style directives over a list of e.g. arguments	191
mc	aug	the mc element can now have a for attribute. It does not allow symbol children any more, if these are needed, the dominating exercise element should have its own theory. Furthermore, the mc element can now have a theory, generated-from, and generated-via attributes.	210
measure	aug	allows an optional xml:id attribute	141
metacomment	dep	This element is superseded by the omtext element.	124

columns: element | aug | The element element now allows the map and separator elements in the body. Furthermore, it carries the optional attributes crid for parallel markup, cr for cross-references, and ns for specifying the namespace. | 190

Table p. 324.69 — 11×4, 0 spanning cell(s)
morphism	aug	The morphism element now carries the optional attributes consistency, exhaustivity, hiding, and type. Furthermore the content model allows optional elements measure and ordering after the requation children to specify termination information like in definition.	92
obligation	aug	allows an optional xml:id attribute	178
omdoc	aug	This element can now have a theory, generated-from, and generated-via attributes.	90
omgroup	cha	The values dataset and labeled-dataset are deprecated in Version 1.2 of OMDoc, since we provide tables in module RT; see Section 14.6 for details. Furthermore, the element can now have the attributes, modules, theory, generated-from, and generated-via.	93
omlet	cha	omlet can no longer occur at top-level (it just does not make sense). The data model for this element has been totally reworked, inspired by the xhtml:object element.	205
omstyle	aug	This element can now have generated-from, and generated-via attributes. New attribute xref that allows to inherit the information from another omstyle element.	188
om:*	aug	with OpenMath2, the OpenMath elements carry an optional id attribute for structure sharing via the om:OMR element. Furthermore, in OMDoc, they carry cref attributes for parallel markup with crossreferences.	108
om: OMFOREIGN	new	The om:OMFOREIGN element can be used to encapsulate arbitrary XML data in OpenMath attributions.	110
om: 0MR	new	In the OpenMath2 standard, this element is the main vehicle of the structure sharing representation.	112
omtext	aug	the type attribute can now also have the values axiom, definition, theorem, proposition, lemma, corollary, postulate, conjecture, false-conjecture, obligation, assumption, and formula. Furthermore, omtext can now have theory, generated-from, and generated-via and verbalizes attributes.	124
ordering	aug	Now allows the optional xml:id and terminating attributes. The latter points to a termination assertion.	141

columns: morphism | aug | The morphism element now carries the optional attributes consistency, exhaustivity, hiding, and type. Furthermore the content model allows optional elements measure and ordering after the requation children to specify termination information like in definition. | 92

Table p. 325.70 — 12×4, 0 spanning cell(s)
output	aug	allows an optional xml:id attribute	204
pattern	aug	this element is no longer used, the pattern of a recursive equation is determined by the position as the first child.
path-just	aug	The element can now appear as a toplevel element, if it does, the attribute for must point to the axiom-inclusion element it justifies. It also now allows an optional xml:id attribute	184
phrase	new	used to mark up phrases in CMPs and supply them with identifiers and links to context that can be used for presentation and referencing.	126
presentation	cha	The theory is not allowed any more, to refer to a symbol outside its theory use its xml:id attribute. The element now also allows a mutilingual CMP group, so that it can be used as a notation definition element in mathematical vernacular.	192
private	cha	The replaces attribute is now called reformulates. The attributes pto and pto-version have moved to the data element. The attribute type has been removed and optional attributes theory, generated-from, and generated-via have been added.	202
proof	lib	The for attribute is now optional to allow for proofs as objects of mathematical discourse. Furthermore, it can now have generated-from and generated-via attributes.	161
proofobject	lib	The for attribute is now optional to allow for proofs as objects of mathematical discourse. Furthermore, it can now have generated-from and generated-via attributes.	169
recognizer	cha	The role attribute was fixed to object. The commonname child has been replaced by an initial metadata element.	157
ref	aug	ref now has an optional xml:id attribute that identifies it.	94
selector	cha	The role attribute was fixed to object. The commonname child has been replaced by an initial metadata element.	157
solution	cha	the solution element now allows arbitrary OMDoc top-level elements as children. Furthermore, it can now have a theory, generated-from, and generated-via attributes.	209

columns: output | aug | allows an optional xml:id attribute | 204

Table p. 326.71 — 8×4, 0 spanning cell(s)
sortdef	cha	The role attribute was fixed to sort. The type from the adt element is now on the sortdef element. The commonname child has been replaced by an initial metadata element.	156
dc:subject	aug	The dc:subject can now have the optional dc:id, and CSS attributes	99
style	aug	The style element now allows a map element in the body	189
symbol	cha	may no longer contain selector, since it only makes sense for constructors in data types. The kind attribute has been renamed to role for compatibility with OpenMath2 and can have the additional values binder, attribution, semantic-attribution, and error corresponding to the OpenMath 2 roles. Furthermore, an optional attribute generated-via has been added to allow generation via a theory morphism.	136
term	new	the term element can appear in mathematical text and contain it. It is used to link technical terms to symbols defined in content dictionaries via its cd and name attributes.	128
theory	cha	the theory element loses the CMP and commonname children, use the Dublin Core metadata elements dc:description and dc:subject instead. The theory element also gains the optional cdbase attribute to specify the disambiguating string prescribed for content dictionaries by the OpenMath2 standard. The xml:id is now optional, it only needs to be specified, if the theory has constitutive elements. Finally, the element has gained the optional attributes cdurl, cdbase, cdreviewdate, cdversion, cdrevision, and cdstatus attributes for encoding the management metadata of OpenMath content dictionaries.	149
dc:title	aug	The dc:title can now have the optional dc:id, and CSS attributes.	98
tgroup	new	The tgroup can be used to structure theories like documents.	149

columns: sortdef | cha | The role attribute was fixed to sort. The type from the adt element is now on the sortdef element. The commonname child has been replaced by an initial metadata element. | 156

Table p. 327.72 — 7×4, 0 spanning cell(s)
type	aug	\begin{tabular}[t]{l} the type element now has the optional just-by and theory attribute. The first one points to an assertion or axiom that justifies the type judgment, the second specifies the home theory. The system attribute is now optional. \\ Furthermore, the type element can have two math objects as children. If it does, then it is a term declaration, i.e. the first element is interpreted as a mathematical object and the second one is interpreted as its type. \\ Finally, it can now have generated-from and generated-via attributes. \end{tabular}	139
theory-inclusion	aug	the theory-inclusion element can now have obligation and decomposition children that justify it. Furthermore, it can now have a theory, generated-from, and generated-via attributes. New optional attributes conservativity and conservativity-just for stating and justifying conservativity.	178
theory	aug	the theory element can now be nested.	149
use	cha	can now contain element, text, recurse, map, and value-of to specify XML content. We have deprecated the larg-group and rarg-group attributes, since they were never used.	194
value	aug	this element is no longer used, the value of a recursive equation is determined by the position as the second child.
with	ren	the role of this element is now taken by the phrase element.	126
xslt	cha	the content of this element need not be escaped any more, it is now a valid XSLT fragment.	189

columns: type | aug | \begin{tabular}[t]{l} the type element now has the optional just-by and theory attribute. The first one points to an assertion or axiom that justifies the type judgment, the second specifies the home theory. The system attribute is now optional. \\ Furthermore, the type element can have two math objects as children. If it does, then it is a term declaration, i.e. the first element is interpreted as a mathematical object and the second one is interpreted as its type. \\ Finally, it can now have generated-from and generated-via attributes. \end{tabular} | 139

Table p. 328.73 — 14×4, 0 spanning cell(s)
element	state	comments	cf.
attribute	new	presentation of attributes for XML elements	191
alternative	cha	new form of the alternative-def element, it can now also used as an alternative to axiom. Compared to alternative-def it has a new optional attribute generated-by to show that an assertion is generated by expanding a some other element like adt.	145
alternative-def	dep	new form is alternative, since there can be alternative axioms too.
argument	cha	attribute sort is now of type IDREF, since it must be local in the definition.	156
assertion	aug	more values for the type attribute, new optional attribute generated-by to show that an assertion is generated by expanding a definition or an adt. New optional attribute proofs.	142
assertion-just	dep	this is now obligation
axiom	aug	new optional attribute generated-by to show that an axiom is generated by expanding a definition.	138
axiom-inclusion	cha	now allows a CMP group for descriptive text, includes a set of obligation elements instead of an assertion-just. The timestamp attribute is deprecated, use dc:date with appropriate action instead	180
CMP	cha	the attribute format is now deprecated, it makes no sense, since we are more strict and consistent about CMP content. CMP now allows an optional id attribute.	122
code	cha	Attributes width and height now in omlet, got attributes classid and codebase from private. Attribute format moved to data children. The multilingual group of CMP elements for description is deprecated, use metadata/dc:description instead. Child element data may appear multiple times (with different values of the format).	202
constructor	aug	new optional child recognizer for a recognizer predicate	156
Coverage	dep	this Dublin Core element specifies the place or time which the publication's contents addresses. This does not seem appropriate for the mathematical content of OMDoc.
data	aug	new optional attributes size to specify the size of the data file that is referenced by the href attribute and format for the format the data is in.	203

columns: element | state | comments | cf.

Table p. 329.74 — 16×4, 0 spanning cell(s)
dc:date	aug	new optional who attribute that can be used to specify who did the action on this date.	99
Translator	dep	this element is not part of Dublin Core, it got into OMDoc by mistake, we use dc:contributor with role=trl for this.	98
decomposition	aug	has a new required id attribute. It is no longer a child of theory-inclusion, but specifies which theory-inclusion it justifies by the new required attribute for.	184
definition	aug	new optional children measure and ordering to specify termination of recursive definitions. New optional attribute generated-by to show that it is generated by expanding a definition.	139
element	new	presentation of XML elements	190
FMP	aug	now allows multiple conclusion elements, to represent general Gentzen-type sequents (not only natural deduction.) FMP now allows an optional id attribute.	123
hypothesis	cha	new required attribute discharged-in to specify the derive element that discharges this hypothesis.	162
measure	new	specifies a measure function (as an OMOBJ)	141
metadata	aug	new optional attribute inherits that allows to inherit metadata from other declarations	92
method	cha	first child that used to be an om:OMSTR or ref element is now moved into a required xref attribute that holds an URI that points to the element that defines the method. The om:OMOBJ content of the other children (they were parameter elements) is now directly included in the method element.	164
obligation	new	takes over the role of assertion-just.
omgroup	aug	also allows the elements that can only appear in theory elements, so that omgroups can also be used for grouping inside theory elements. The type attribute is now restrained to one of narrative, sequence, alternative, contrast.	93
omlet	aug	obtained attributes width and height from private. New optional attributes action for the action to be taken when activated, and data a URIref to data in a private element. New optional attribute type for the type of the applet.	205
omstyle	new	for specifying the style of OMDoc elements	188
omtext	cha	the from is deprecated, we only leave the for attribute, to specify the referential character of the type.	124
ordering	new	specifies a well-founded ordering (as an OMOBJ)	141

columns: dc:date | aug | new optional who attribute that can be used to specify who did the action on this date. | 99

Table p. 330.75 — 13×4, 0 spanning cell(s)
parameter	dep	the om:OMOBJ element child is now directly a child of method
pattern	cha	the child can be an arbitraryOpenMath element.
premise	cha	new optional attribute rank for the importance in the inference rule. The old href attribute is renamed to xref to be consistent with other cross-referencing.
presentation	aug	\begin{tabular}[t]{l} New attribute xref that allows to inherit the information from another presentation element. New attribute theory to specify the theory the symbol is from; without this, referencing in OMDoc is not unique. \\ The parent attribute has been renamed to role and now takes the values applied, binding, and key, since we want to be less OpenMath-centric \end{tabular}	192
private	cha	\begin{tabular}[t]{l} new optional attribute for to point to an OMDoc element it provides data for. As a consequence, private elements are no longer allowed in other OMDoc elements, only on top-level. New attribute replaces as a pointer to the OMDoc elements that are replaced by the system-specific information in this element. Old attributes width and height now in omlet. Attribute format moved to data children. \\ The descriptive CMP elements are deprecated, use metadata/dc:description instead. \\ Child element data may appear multiple times (with different values of the format). The attributes classid and codebase are deprecated, since they only make sense on the code element. \end{tabular}	q 202
proof	cha	attribute theory is now optional, since the element can appear inside a theory element.	161
proofobject	cha	attribute theory is now optional, since the element can appear inside a theory element.	161
recognizer	new	specifies the recognizer predicate of a sort.	157
recurse	new	recursive calls to presentation in style.	191
ref	cha	attribute kind renamed to type.	94
selector	cha	the old type attribute (had values total and partial) is deprecated, its duty is now carried by an attribute total (values yes and no).	157
signature	dep	for the moment
sortdef	cha	has a mandatory name attribute, otherwise the defined symbol has no name.	156

columns: parameter | dep | the om:OMOBJ element child is now directly a child of method |

Table p. 331.76 — 9×4, 0 spanning cell(s)
style	new	allows to specify style information in presentation and omstyle elements using a simplified OMDoc-internalized version of XSLT.	189
symbol	aug	new optional attribute generated-by to show that it is generated by expanding a definition.	136
text	new	presentation of text in omstyle.	190
theory-inclusion	cha	now allows CMP group for descriptive text, no longer has a decomposition child, this is now attached by its for attribute. The timestamp attribute is deprecated, use dc:date with appropriate action instead.	178
type	aug	can now also appear on top-level. Has an optional id attribute for identification, and an optional for attribute to point to a symbol element it declares type information for.	139
use	aug	New attribute element allows to specify that the content should be encased in an XML element with the attribute-value pairs specified in the string specified in the attribute attributes.	194
value-of	new	presentation of values in style.	190
with	new	used to supply fragments of text in CMPs with style and id attributes that can be used for presentation and referencing.	126
xslt	new	allows to embed XSLT into presentation and omstyle elements.	189

columns: style | new | allows to specify style information in presentation and omstyle elements using a simplified OMDoc-internalized version of XSLT. | 189

Table p. 332.77 — 2×7, 0 spanning cell(s)
Element	p.	Mod.	Required	Optional	D	Content
Attribs	Attribs	C

columns: Element | p. | Mod. | Required | Optional | D | Content

Table p. 332.78 — 10×7, 0 spanning cell(s)
adt	156	ADT	xml:id, type, style, class, theory, generated-from, generated-via	+	sortdef+
alternative	145	ST	for, entailed-by, entails, entailed-by-thm, entails-thm	xml:id, type, theory, generated-from, generated-via, uniqueness, exhaustivity, consistency, existence, style, class	+	CMP, (FMP\| requation\| (OMOBJ \|m:math \|legacy)*)
answer	210	QUIZ	verdict	xml:id, style, class	+	CMP, FMP
m:apply	115	MML	id, xlink:href	-	bvar?, 《CMel》*
argument	156	ADT	sort	+	selector?
assertion	142	ST	xml:id, type, theory, generated-from, generated-via, style, class	+	CMP, FMP
assumption	124	MTXT	xml:id, inductive, style, class	+	CMP*, (OMOBJ \|m:math \|legacy)?
attribute	191	PRES	name	-	(value-of\| text)*
axiom	138	ST	name	xml:id, type, generated-from, generated-via, style, class	+	CMP, FMP
axiom-inclusion	180	CTH	from, to	xml:id, style, class, theory, generated-from, generated-via	+	morphism?, (path-just\| obligation*)

columns: adt | 156 | ADT | | xml:id, type, style, class, theory, generated-from, generated-via | + | sortdef+

Table p. 332.79 — 4×6, 0 spanning cell(s)
m:bvar	115	MML	id, xlink:href	-	ci*
m:ci	115	MML	id, xlink:href	-	PCDATA
m : cn	115	MML	id, xlink:href	-	\[ \begin{aligned} & ([0-9]\|,\| .) \\ & (* \mid \mathrm{e}([0-9]\|,\| .) *) ? \end{aligned} \]
choice	210	QUIZ	xml:id, style, class	+	CMP, FMP

columns: m:bvar | 115 | MML | id, xlink:href | - | ci*

Table p. 333.80 — 6×7, 0 spanning cell(s)
CMP	122	MTXT	xml：lang，xml：id	－	（text｜OMOBJ｜m：math ｜legacy｜with｜term ｜omlet）＊
code	202	EXT	xml：id， for，theory， generated－from， generated－via， requires，style， class	＋	input？，output？， effect？，data＋
conclusion	124	MTXT	xml：id，style， class	＋	CMP＊，（OMOBJ｜m：math ｜legacy）？
constructor	156	ADT	name	type，scope， style，class， theory， generated－from， generated－via	＋	argument＊，recognizer？
dc：contributor	98	DC	xml：id，role， style，class	－	《text》
dc：creator	98	DC	xml：id，role， style，class	－	《text》

Table p. 333.81 — 11×7, 0 spanning cell(s)
m：csymbol	115	MML	definitionURL	id，xlink：href	－	EMPTY
data	203	EXT	format，href， size，original	－	＜！［CDATA［．．．］］＞
dc：date	99	DC	action，who	－	ISO 8601 norm
dd	130	RT	xml：id，style， class，index， verbalizes	＋	CMPcontent
di	130	RT	xml：id，style， class，index， verbalizes	＋	dt＋，dd＊
dl	130	RT	xml：id，style， class，index， verbalizes	＋	li＊
dt	130	RT	xml：id，style， class，index， verbalizes	＋	CMPcontent
decomposition	184	DG	links	theory， generated－from， generated－via	－	EMPTY
definition	139	ST	xml：id，for	uniqueness， existence， consistency， exhaustivity， type， generated－from， generated－via， style，class	＋	CMP＊，（FMP｜ requation＋｜OMOBJ ｜m：math｜legacy）？， measure？，ordering？
dc：description	99	DC	xml：lang	－	CMPcontent
derive	162	PF	xml：id，style， class	－	CMP＊，FMP？，method？

columns: m：csymbol | 115 | MML | definitionURL | id，xlink：href | － | EMPTY

Table p. 333.82 — 3×7, 0 spanning cell(s)
effect	204	EXT	xml：id，style， class	－	CMP＊，FMP＊
element	190	PRES	name	xml：id，cr，ns	－	（attribute｜element｜ text｜recurse）＊
example	146	ST	for	xml：id，type， assertion， proof，style， class，theory， generated－from， generated－via	＋	CMP＊｜（OMOBJ｜m：math ｜legacy）？

columns: effect | 204 | EXT | | xml：id，style， class | － | CMP＊，FMP＊

Table p. 334.83 — 3×7, 0 spanning cell(s)
exercise	209	QUIZ	xml:id, type, for, from, style, class, theory, generated-from, generated-via	+	CMP, FMP, hint?, (solution\|mc)
FMP	123	MTXT	logic, xml:id	-	(assumption, conclusion) \|OMOBJ \|m:math \|legacy
dc:format	100	DC	-	fixed: "application/omdoc+xml"

columns: exercise | 209 | QUIZ | | xml:id, type, for, from, style, class, theory, generated-from, generated-via | + | CMP*, FMP*, hint?, (solution*|mc*)

Table p. 334.84 — 2×7, 0 spanning cell(s)
hint	209	QUIZ	xml:id, style, class, theory, generated-from, generated-via	+	CMP, FMP
hypothesis	162	PF	xml:id, style, class, inductive	-	CMP, FMP

Table p. 334.85 — 10×7, 0 spanning cell(s)
dc:identifier	100	DC	scheme	-	ANY
ide	130	RT	index	xml:id,sort-by,see seealso, links, style, class	-	idp*
idp	130	RT	xml:id,sort-by,see seealso, links, style, class	-	CMPcontent
idt	130	RT	style, class	-	CMPcontent
idx	130	RT	xml:id,sort-by,see seealso, links, style, class	-	idt?,idp+
ignore	92	DOC	type, comment	-	ANY
imports	150	CTH	from	xml:id, type, style, class	+	morphism?
inclusion	179	CTH	for	xml:id	-
input	204	EXT	xml:id, style, class	-	CMP* , FMP*
insort	156	ADT	for	-

columns: dc:identifier | 100 | DC | | scheme | - | ANY

Table p. 334.86 — 2×7, 0 spanning cell(s)
dc:language	100	DC	-	ISO 8601 norm
li	130	RT	xml:id, style, class, index, verbalizes	-	Math Vernacular

columns: dc:language | 100 | DC | | | - | ISO 8601 norm

Table p. 334.87 — 8×7, 0 spanning cell(s)
cc:license	102	CC	jurisdiction	-	permissions, prohibitions, requirements
link	130	RT	xml:id, style, class, index, verbalizes	-	Math Vernacular
m:math	114	MML	id, xlink:href	-	《CMel》+
mc	210	QUIZ	xml:id, style, class, theory, generated-from, generated-via	-	choice, hint?, answer
measure	141	ST	xml:id	-	OMOBJ \|m:math \|legacy
metadata	92	DC	inherits	-	(dc-element) *
method	164	PF	xref	-	(OMOBJ \|m:math \|legacy\| premise \| proof \| proofobject)*
morphism	175	CTH	xml:id, base, consistency, exhaustivity, type, hiding, style, class	-	requation*, measure?, ordering?

columns: cc:license | 102 | CC | | jurisdiction | - | permissions, prohibitions, requirements

Table p. 334.88 — 1×7, 0 spanning cell(s)
note	131	RT	type,xml:id, style, class, index, verbalizes	-	Math Vernacular

columns: note | 131 | RT | | type,xml:id, style, class, index, verbalizes | - | Math Vernacular

Table p. 335.89 — 23×7, 0 spanning cell(s)
obligation	178	CTH	induced－by， assertion	xml：id	－	EMPTY
om：0MA	108	OM	id，cdbase	－	《OMel》＊
om：OMATTR	110	OM	id，cdbase	－	《OMel》
om：OMATP	110	OM	cdbase	－	（OMS，（《OMel》）I om：OMFOREIGN））＋
om ：0MB	111	OM	id，class，style， class	－	＃PCDATA
om：OMBIND	109	OM	id，cdbase	－	《OMel》，om：OMBVAR，《OMel》？
om ：OMBVAR	109	OM	－	（om：OMV｜om：OMATTR）＋
om：OMFOREIGN	110	OM	id，cdbase	－	ANY
omdoc	90	DOC	xml：id，type， version， style，class， xmlns，theory， generated－from， generated－via	＋	（top－level element）＊
om：0ME	111	OM	xml：id	－	（《OMel》））？
om：0MR	112	OM	href	－
om ：0MF	111	OM	id，dec，hex	－	＃PCDATA
omgroup	93	DOC	xml：id，type， style，class， modules，theory， generated－from， generated－via	＋	top－level element＊
ol	130	RT	xml：id，style， class，index， verbalizes	—	li＊
om：0MI	111	OM	id，class，style	－	［0－9］＊
omlet	205	EXT	id，argstr，type， function，action， data，style， class	＋	ANY
om：0M0BJ	108	OM	id，cdbase， class，style	－	《（OMel）〉？
omstyle	188	PRES	element	for，xml：id， xref，style， class	－	（style｜xslt）＊
om：0MS	108	OM	cd，name	class，style	－	EMPTY
omtext	124	MTXT	xml：id，type， for，from， style，theory， generated－from， generated－via	＋	CMP＋，FMP？
om：0MV	108	OM	name	class，style	－	EMPTY
ordering	141	ST	xml：id	－	OMOBJ｜m：math｜legacy
output	204	EXT	xml：id，style， class	－	CMP＊，FMP＊

columns: obligation | 178 | CTH | induced－by， assertion | xml：id | － | EMPTY

Table p. 335.90 — 5×7, 0 spanning cell(s)
p	130	RT	xml：id，style， class，index， verbalizes	－	Math Vernacular
param	207	EXT	name	value，valuetype	－	EMPTY
path－just	184	DG	local，globals	for，xml：id	－	EMPTY
cc：permissions	103	CC	reproduction， distribution， derivative＿works	－	EMPTY
premise	164	PF	xref	－	EMPTY

columns: p | 130 | RT | | xml：id，style， class，index， verbalizes | － | Math Vernacular

Table p. 336.91 — 6×7, 0 spanning cell(s)
presentation	192	PRES	for	xml:id, xref, fixity, role, lbrack, rbrack, separator, bracket-style, style, class, precedence, crossref-symbol	-
private	202	EXT	xml:id, for, theory, generated-from, generated-via, requires, reformulates, style, class	+	data+
cc:prohibitions	103	CC	commercial_use	-	EMPTY
proof	161	PF	xml:id, for,theory, generated-from, generated-via, style, class	+	(symbol \| definition \| omtext \| derive \| hypothesis)*
proofobject	169	PF	xml:id, for, theory, generated-from, generated-via, style, class	+	CMP*, (OMOBJ \|m:math \|legacy)
dc:publisher	99	DC	xml:id, style, class	-	ANY

columns: presentation | 192 | PRES | for | xml:id, xref, fixity, role, lbrack, rbrack, separator, bracket-style, style, class, precedence, crossref-symbol | - | (use | xslt | style)*

Table p. 336.92 — 7×7, 0 spanning cell(s)
ref	94	DOC	xref, type	-	ANY
recognizer	157	ADT	name	type, scope, role, style, class	+
recurse	191	PRES	select	-	EMPTY
dc:relation	100	DC	-	ANY
requation	140	ST	xml:id, style, class	—	(OMOBJ \|m:math \|legacy), (OMOBJ \|m:math \|legacy)
cc:requirements	103	CC	notice, copyleft, attribution	—	EMPTY
dc:rights	100	DC	-	ANY

columns: ref | 94 | DOC | | xref, type | - | ANY

Table p. 336.93 — 7×7, 0 spanning cell(s)
selector	157	ADT	name	type, scope, role, total, style, class	+
solution	209	QUIZ	xml:id, for, style, class, theory, generated-from, generated-via	+	(CMP, FMP) \| proof
sortdef	156	ADT	name	role, scope, style, class	+	(constructor\|insort)*
dc:source	100	DC	-	ANY
style	189	PRES	format	xml:lang, requires	-	(element \| text \| recurse \| value-of)*
dc:subject	99	DC	xml:lang	-	CMPcontent
symbol	136	ST	name	role, scope, style, class, generated-from, generated-via	+	type*

columns: selector | 157 | ADT | name | type, scope, role, total, style, class | + |

Table p. 336.94 — 2×7, 0 spanning cell(s)
table	130	RT	xml:id, style, class, index, verbalizes	-	tr*
term	128	MTXT	cd, name	xml:id, role, style, class	-	CMP content

columns: table | 130 | RT | | xml:id, style, class, index, verbalizes | - | tr*

Table p. 337.95 — 10×7, 0 spanning cell(s)
text	190	PRES	-	\#PCDATA
td	130	RT	xml:id, style, class, index, verbalizes	-	Math Vernacular
th	130	RT	xml:id, style, class, index, verbalizes	-	Math Vernacular
theory	149	ST	xml:id	cdbase, style, class	+	(statement/theory)*
theory-inclusion	178	CTH	from, to	xml:id, style, class, theory, generated-from, generated-via	+	(morphism, decomposition?)
tr	130	RT	xml:id, style, class, index, verbalizes	-	(td\|th)*
dc:title	98	DC	xml:lang	-	CMPcontent
tgroup	149	DOC	xml:id, type, style, class, modules, generated-from, generated-via	+	top-level or theoryconstitutive element*
type	139	ST	system	xml:id, for, style, class	-	CMP*, (OMOBJ \|m:math \|legacy)
dc:type	100	DC	-	fixed: "Dataset" or "Text" or "Collection"

Table p. 337.96 — 5×7, 0 spanning cell(s)
ul	130	RT	xml:id, style, class, index, verbalizes	-	li*
use	194	PRES	format	xml:lang, requires, fixity, lbrack, rbrack, separator, crossref-symbol, element, attributes	-	(use \| xslt \| style)*
value-of	190	PRES	select	-	EMPTY
phrase	126	MTXT	xml:id, style, class, index, verbalizes, type	-	CMP content
xslt	189	PRES	format	xml:lang, requires	-	XSLT fragment

columns: ul | 130 | RT | | xml:id, style, class, index, verbalizes | - | li*

Table p. 338.97 — 33×3, 9 spanning cell(s)
Attribute	element	Values
action	dc:date	unspecified
specifies the action taken on the document on this date.
action	omlet	execute, display, other
specifies the action to be taken when executing the omlet, the value is application-defined.
actuate	omlet	onPresent, onLoad, onRequest, other
specifies the timing of the action specified in the action attribute
assertion	example
specifies the assertion that states that the objects given in the example really have the expected properties.
assertion	obligation
specifies the assertion that states that the translation of the statement in the source theory specified by the induced-by attribute is valid in the target theory.
attributes	use
the attribute string for the start tag of the XML element substituted for the brackets (this is specified in the element attribute).
attribution	cc:requirements	required, not_required
Specifies whether the copyright holder/author must be given credit in derivative works
base	morphism
specifies another morphism that should be used as a base for expansion in the definition of this morphism
bracket-style	presentation, use	lisp, math
specifies whether a function application is of the form \(f(a, b)\) or ( \(f a b\) )
cd	om: 0MS
specifies the content dictionary of an OpenMath symbol
cd	term
specifies the content dictionary of a technical term
cdbase	om: *
specifies the base URI of the content dictionaries used in an OpenMath object
cdreviewdate	theory
specifies the date until which the content dictionary will remain unchanged
cdrevision	theory
specifies the minor version number of the content dictionary
cdstatus	theory	official, experimental, private, obsolete
specifies the content dictionary status
cdurl	theory
found	the main URL, where the newest version of the content dictionary can be

columns: Attribute | element | Values

Table p. 339.98 — 47×3, 14 spanning cell(s)
cdversion	theory
specifies the major version number of the content dictionary
comment	ignore
specifies a reason why we want to ignore the contents
crossref-symbol	presentation, use	all, brackets, lbrack, no, rbrack, separator, yes
specifies whether cross-references to the symbol definition should be generated in the output format.
class	*
specifies the CSS class
commercial_use	cc:permissions	permitted, prohibited
specifies, whether commercial use of the document with this license is permitted
consistency	morphism, definition	OMDoc reference
points to an assertion stating that the cases are consistent, i.e. that they give the same values, where they overlap
copyleft	cc:restrictions	required, not_required
specifies whether derived works must be licensed with the same license as the current document.
cr	element	yes/no
specifies whether an xlink:href cross-reference should be set on the result element.
cref	om: *	URI reference
extra attribute for cross-references in parallel markup
crid	element	XPath expression
the path to the sub-element that corresponds to the result element.
crossref-symbol	presentation, use	no, yes, brackets, separator, lbrack, rbrack, all
specifies which generated presentation elements should carry crossreferences to the definition.
data	omlet
points to a private element that contains the data for this omlet
definitionURL	m: *	URI
points to the definition of a mathematical concept
derivative_works	cc:permissions	permitted, not_permitted
specifies whether the document may be used for making derivative works.
distribution	cc:permissions	permitted, not_permitted
specifies whether distribution of the current document fragment is permitted.
element	use
the XML element tags to be substituted for the brackets.
element	omstyle
the XML element, the presentation information contained in the omstyle element should be applied to.
encoding	m:annotation,om:0MF0REIGN	MIME type of the content
specifies the format of the content
entails, entailed-by	alternative
specifies the equivalent formulations of a definition or axiom
entails-thm, entailed-by-thm	alternative
specifies the entailment statements for equivalent formulations of a definition or axiom
exhaustivity	morphism, definition	OMDoc reference
points to an assertion that states that the cases are exhaustive.
existence	definition	OMDoc reference
points to an assertion that states that the symbol described in an implicit
fixity	presentation	assoc, infix, postfix, prefix
specifies where the function symbol-of a function application should be
function	omlet

columns: cdversion | theory |

Table p. 340.99 — 50×3, 16 spanning cell(s)
specifies the function to be called when this omlet is activated.
format	data
specifies the format of the data specified by a data element. The value should e.g. be a MIME type [FB96].
for	*
can be used to reference an element by its unique identifier given in its xml:id attribute.
formalism	legacy	URI reference
specifies the formalism in which the content is expressed
format	legacy	URI reference
specifies the encoding format of the content
format	use	cmml, default, html, mathematica, pmml, TeX,...
specifies the output format for which the notation is specified
from	imports, theory-inclusion, axiom-inclusion	URI reference
pointer to source theory of a theory morphism
from	omtext	URI reference
points to the source of a relation given by a text type
generated-from	top-level elements	URI reference
points to a higher-level syntax element, that generates this statement.
generated-via	top-level elements,...	URI reference
points to a theory-morphism, via which it is translated from the element pointed to by the generated-from attribute.
globals	path-just
points to the axiom-inclusions or theory-inclusions that is the rest of the inclusion path.
hiding	morphism
specifies the names of symbols that are in the domain of the morphism
href	data, link, om:OMR	URI reference
a URI to an external file containing the data.
xml:id
\begin{tabular}[t]{l} associates a unique identifier to an element, which can thus be referenced \\ associates a unique identifier to an element, which can thus be referenced by an for or xref attribute. \end{tabular}
xml:base
specifies a base URL for a resource fragment
index	on RT elements
A path identifier to establish multilingual correspondence
induced-by	obligation
points to the statement in the source theory that induces this proof obligation
inductive	assumption, hypothesis	yes, no
Marks an assumption or hypothesis inductive.
inherits	metadata	URI reference
points to a metadata element from which this one inherits.
jurisdiction	cc:license	IANA Top level Domain designator
specifies the country of jurisdiction for a Creative Commons license
just-by	type
points to an assertion that states the type property in question.
role	symbol, constructor, recognizer, selector, sortdef	object, type, sort, binder, attribution, semantic-attribution, error
specifies the role (possible syntactic roles) of the symbol in this declaration.
role	dc:creator,dc:contributor	MARC relators
specifies the role of a person who has contributed to the document
role	presentation	applied, binding, key
specifies which role of the symbol is annotated with notation information
lbrack	presentation, use
the left bracket to use in the notation of a function symbol
links	decomposition

columns: format | specifies the function to be called when this omlet is activated. data | specifies the function to be called when this omlet is activated.

Table p. 341.100 — 49×3, 11 spanning cell(s)
specifies a list of theory- or axiom-inclusions that justify (by decomposition) the theory-inclusion specified in the for attribute.
local	path-just
points to the axiom-inclusion that is the first element in the path.
logic	FMP	token
specifies the logical system used to encode the property.
modules	omdoc, omgroup	module and sub-language shorthands, URI reference
specifies the modules or OMDoc sub-language used in this document fragment
name	om:OMS, om:OMV, symbol, term
the name of a concept referenced by a symbol, variable, or technical term.
name	attribute, element
the local name of generated element.
name	param
the name of a parameter for an external object.
notice	cc:requirements	required, not_required
specifies whether copyright and license notices must be kept intact in distributed copies of this document
ns	element, attribute	URI
specifies the namespace URI of the generated element or attribute node
original	data	local, external
specifies whether the local copy in the data element is the original or the external resource pointed to by the href attribute.
parameters	adt
The list of formal parameters of a higher-order abstract data type
precedence	presentation
the precedence of a function symbol (for elision of brackets)
proofs	assertion
specifies a list of URIs to proofs of this assertion.
pto, pto-version	private, code
specifies the system and its version this data or code is private to
rank	premise
specifies the rank (importance) of a premise
rbrack	presentation, use
the right bracket to use in the notation of a function symbol
reformulates	private
points to a set of elements whose content is reformulated by the content of the private element for the system.
reproduction	cc:permissions	permitted, not_permitted
specifies whether reproduction of the current document fragment is permitted by the licensor
requires	private, code, use, xslt, style	URI reference
points to a code element that is needed for the execution of this data by the system.
role	dc:creator, dc:collaborator	aft, ant, aqt, aui, aut, clb, edt, ths, trc, trl
the MARC relator code for the contribution of the individual.
role	phrase, term
the role of the phrase annotation
role	presentation	applied, binding, key
specifies for which role (as the head of a function application, as a binding symbol, or as a key in a attribution, or as a stand-alone symbol (the default)) of the symbol presentation is intended
scheme	dc:identifier	scheme name
specifies the identification scheme (e.g. ISBN) of a resource
scope	symbol	global, local
\begin{tabular}[t]{l} specifies the visibility of the symbol declared. This is a very crude specifi- \\ specifies the visibility of the symbol declared. This is a very crude specification, it is better to use theories and importing to specify symbol accessibility. \end{tabular}
select	map, recurse, value-of	XPath expression
specifies the path to the sub-expression to act on

columns: local | specifies a list of theory- or axiom-inclusions that justify (by decomposition) the theory-inclusion specified in the for attribute. path-just | specifies a list of theory- or axiom-inclusions that justify (by decomposition) the theory-inclusion specified in the for attribute.

Table p. 342.101 — 45×3, 13 spanning cell(s)
separator	presentation, use
the separator for the arguments to use in the notation of a function symbol
show	omlet	new, replace, embed, other
specifies the desired presentation of the external object.
size	data
specifies the size the data specified by a data element. The value should be number of kilobytes
sort	argument
specifies the argument sort of the constructor
style	*
specifies a token for a presentation style to be picked up in a presentation element.
system	type
A token that specifies the logical type system that governs the type specified in the type element.
theory	*
specifies the home theory of an OMDoc statement.
to	theory-inclusion, axiom-inclusion
specifies the target theory
total	selector	no, yes
specifies whether the symbol declared here is a total or partial function.
type	adt	free, generated, loose
defines the semantics of an abstract data type free = no junk, no confusion, generated = no junk, loose is the general case.
type	assertion	theorem, lemma, corollary, conjecture, false-conjecture, obligation, postulate, formula, assumption, proposition
tells you more about the intention of the assertion
type	definition	implicit, inductive, obj, recursive, simple
specifies the definition principle
type	derive	conclusion, gap
singles out special proof steps: conclusions and gaps (unjustified proof steps)
type	example	against, for
specifies whether the objects in this example support or falsify some conjecture
type	ignore
specifies the type of error, if ignore is used for in-place error markup
type	imports	global, local
local imports only concern the assumptions directly stated in the theory. global imports also concern the ones the source theory inherits.
type	morphism
specifies whether the morphism is recursive or merely pattern-defined
type	omgroup, omdoc	enumeration, sequence, itemize
the first three give the text category, the second three are used for generalized tables
type	omtext	abstract, antithesis, comment, conclusion, elaboration, evidence, introduction, motivation, thesis
a specification of the intention of the text fragment, in reference to context.
type	phrase
the linguistic or mathematical type of the phrase
type	ref	include, cite
specifies whether to replace the ref element by the fragment referenced
uniqueness	definition	URI reference
points to an assertion that states the uniqueness of the concept described
value	param

columns: separator | presentation, use |

Table p. 343.102 — 25×3, 11 spanning cell(s)
specifies the value of the parameter
valuetype	param
specifies the type of the value of the parameter
verbalizes	on RT elements	URI references
contains a whitespace-separated list of pointers to OMDoc elements that are verbalized
verdict	answer
specifies the truth or falsity of the answer. This can be used e.g. by a grading application.
version	omdoc	1.2
specifies the version of the document, so that the right DTD is used
version	cc:license
specifies the version of the Creative Commons license that applies, if not present, the newest one is assumed
via	inclusion
points to a theory-inclusion that is required for an actualization
who	dc:date
specifies who acted on the document fragment
xml:lang	CMP, dc:*	ISO 639 code
the language the text in the element is expressed in.
xml:lang	use, xslt, style	whitespace-separated list of ISO 639 codes
specifies for which language the notation is meant
xlink:*	om:OMR, m:*	URI reference
specify the link behavior on the elements
xref	ref, method, premise	URI reference
Identifies the resource in question
xref	presentation, omstyle	URI reference
The element, this URI points to should be in the place of the object containing this attribute.

columns: valuetype | specifies the value of the parameter param | specifies the value of the parameter