<!ELEMENT Conjecture %sequent;>
<!ATTLIST Conjecture
- no NMTOKEN #REQUIRED>
+ no NMTOKEN #REQUIRED
+ id ID #REQUIRED>
<!ELEMENT Constructor %term;>
<!ATTLIST Constructor
<!ELEMENT Decl %term;>
<!ATTLIST Decl
- name CDATA #IMPLIED>
+ name CDATA #IMPLIED
+ id ID #REQUIRED>
<!ELEMENT Def %term;>
<!ATTLIST Def
- name CDATA #IMPLIED>
+ name CDATA #IMPLIED
+ id ID #REQUIRED>
<!ELEMENT Hidden EMPTY>
+<!ATTLIST Hidden
+ id ID #REQUIRED>
<!ELEMENT Goal %term;>