+<!ELEMENT ht:AXIOM (Axiom)>
+<!ATTLIST ht:AXIOM
+ uri CDATA #REQUIRED
+ as (Axiom|Declaration) #REQUIRED>
+
+<!ELEMENT ht:DEFINITION (Definition|InductiveDefinition)>
+<!ATTLIST ht:DEFINITION
+ uri CDATA #REQUIRED
+ as (Definition|InteractiveDefinition|Inductive|CoInductive
+ |Record) #REQUIRED>
+
+<!ELEMENT ht:THEOREM (type)>
+<!ATTLIST ht:THEOREM
+ uri CDATA #REQUIRED
+ as (Theorem|Lemma|Corollary|Fact|Remark) #REQUIRED>
+
+<!ELEMENT ht:VARIABLE (Variable)>
+<!ATTLIST ht:VARIABLE
+ uri CDATA #REQUIRED
+ as (Assumption|Hypothesis|LocalDefinition|LocalFact) #REQUIRED>