Conjectures and Hypotheses inside every conjecture and in the sequents now

[helm.git] / helm / dtd / cic.dtd

diff --git a/helm/dtd/cic.dtd b/helm/dtd/cic.dtd
index 088c78abf4e866db8ca82d1604cebe9619de4a9b..47280b845aa191e8359c5ae42b109340679dfc98 100644 (file)
--- a/helm/dtd/cic.dtd
+++ b/helm/dtd/cic.dtd
@@ -91,7 +91,8 @@
 
 <!ELEMENT Conjecture %sequent;>
 <!ATTLIST Conjecture
-          no NMTOKEN #REQUIRED>
+          no NMTOKEN #REQUIRED
+          id ID      #REQUIRED>
 
 <!ELEMENT Constructor %term;>
 <!ATTLIST Constructor
@@ -99,13 +100,17 @@
 
 <!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;>