<!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