X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fdtd%2Fcicobject.dtd;h=d78251c1d99b25c2dc1ef7745aa6ee66a3cd783f;hb=3c7ca719c304eb7de7d8d4e9a90ebe0db8d8ecab;hp=9514103e45339159e9a2aa7a11db719a2a660879;hpb=638ea30787cd4b14a27fabac36c1319bc6ab14b7;p=helm.git

diff --git a/helm/dtd/cicobject.dtd b/helm/dtd/cicobject.dtd
index 9514103e4..d78251c1d 100644
--- a/helm/dtd/cicobject.dtd
+++ b/helm/dtd/cicobject.dtd
@@ -67,6 +67,10 @@
           name CDATA #REQUIRED
           xmlns:m    CDATA      #REQUIRED>
 
+<!ELEMENT Sequent ((Decl|Def)*,Goal)>
+<!ATTLIST Sequent
+          id   ID    #REQUIRED>
+
 <!-- Elements used in CIC objects, which are not terms: -->
 
 <!ELEMENT InductiveType (arity,Constructor*)>
@@ -88,6 +92,16 @@
 
 <!ELEMENT Params (#PCDATA)*>
 
+<!ELEMENT Decl %term;>
+<!ATTLIST Decl
+          name CDATA #REQUIRED>
+
+<!ELEMENT Def %term;>
+<!ATTLIST Def
+          name CDATA #REQUIRED>
+
+<!ELEMENT Goal %term;>
+
 <!-- Sintactic sugar for CIC objects: -->
 
 <!ELEMENT type  %term;>