+<!ENTITY % theorystructure '(THEOREM|LEMMA|COROLLARY|AXIOM|FACT|DEFINITION|
+ VARIABLE|SECTION)*'>
+
+<!-- Theory -->
+
+<!ELEMENT Theory (%theorystructure;)>
+<!ATTLIST Theory
+ name CDATA #REQUIRED
+ uri CDATA #REQUIRED>
+
+<!-- Theory Items -->
+
+<!ELEMENT THEOREM (type)>
+<!ATTLIST THEOREM
+ name CDATA #REQUIRED
+ uri CDATA #REQUIRED>
+
+<!ELEMENT LEMMA (type)>
+<!ATTLIST LEMMA
+ name CDATA #REQUIRED
+ uri CDATA #REQUIRED>
+
+<!ELEMENT COROLLARY (type)>
+<!ATTLIST COROLLARY
+ name CDATA #REQUIRED
+ uri CDATA #REQUIRED>
+
+<!ELEMENT AXIOM (Axiom)>
+<!ATTLIST AXIOM
+ name CDATA #REQUIRED
+ uri CDATA #REQUIRED>
+
+<!ELEMENT FACT (type)>
+<!ATTLIST FACT
+ name CDATA #REQUIRED
+ uri CDATA #REQUIRED>
+
+<!ELEMENT DEFINITION (Definition|InductiveDefinition)>
+<!ATTLIST DEFINITION
+ name CDATA #REQUIRED
+ uri CDATA #REQUIRED>
+
+<!ELEMENT VARIABLE (Variable)>
+<!ATTLIST VARIABLE
+ name CDATA #REQUIRED
+ uri CDATA #REQUIRED>