ht:DEFINITION/Definition and
ht:DEFINITION/InteractiveDefinition
because of an explicit request of Iris Loeb.
<!ELEMENT ht:DEFINITION (Definition|InductiveDefinition)>
<!ATTLIST ht:DEFINITION
uri CDATA #REQUIRED
<!ELEMENT ht:DEFINITION (Definition|InductiveDefinition)>
<!ATTLIST ht:DEFINITION
uri CDATA #REQUIRED
- as (Definition|Inductive|CoInductive|Record) #REQUIRED>
+ as (Definition|InteractiveDefinition|Inductive|CoInductive
+ |Record) #REQUIRED>
<!ELEMENT ht:THEOREM (type)>
<!ATTLIST ht:THEOREM
<!ELEMENT ht:THEOREM (type)>
<!ATTLIST ht:THEOREM