]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/xml/ld.dtd
when sort inclusion is enabled, we can produce conversion constraints in xml
[helm.git] / helm / software / lambda-delta / xml / ld.dtd
index 00ea552390957f679b48be29da32b26143e170ba..d97173d8279fb5202bef9542f2998f1a3abadc6b 100644 (file)
 
 <!ENTITY % term '(%node;*,%leaf;)'>
 
+<!ENTITY % terms '(%term;*)'>
+
 <!ELEMENT Sort EMPTY>
 <!ATTLIST Sort
           position NMTOKEN #REQUIRED
-          name     CDATA   #IMPLIED
+          name     NMTOKEN #IMPLIED
+          mark     NMTOKEN #IMPLIED
+         meta     CDATA   #IMPLIED
 >
 
 <!ELEMENT LRef EMPTY>
 <!ATTLIST LRef
           position NMTOKEN #REQUIRED
-          name     CDATA   #IMPLIED
+         offset   NMTOKEN #IMPLIED
+          name     NMTOKEN #IMPLIED
+          mark     NMTOKEN #IMPLIED
+         meta     CDATA   #IMPLIED
 >
 
 <!ELEMENT GRef EMPTY>
 <!ATTLIST GRef
-          uri  CDATA #REQUIRED
-          name CDATA #IMPLIED
+          uri  CDATA   #REQUIRED
+          name NMTOKEN #IMPLIED
+          mark NMTOKEN #IMPLIED
+         meta CDATA   #IMPLIED
 >
 
 <!ELEMENT Cast %term;>
 <!ATTLIST Cast
-          name CDATA #IMPLIED
+          arity NMTOKEN #IMPLIED
+          mark  NMTOKEN #IMPLIED
+         meta  CDATA   #IMPLIED
 >
 
-<!ELEMENT Appl %term;>
+<!ELEMENT Appl %terms;>
 <!ATTLIST Appl
-          name CDATA #IMPLIED
+          arity NMTOKEN #IMPLIED
+          mark  NMTOKEN #IMPLIED
+         meta  CDATA   #IMPLIED
 >
 
-<!ELEMENT Abst %term;>
+<!ELEMENT Abst %terms;>
 <!ATTLIST Abst
-          name CDATA #IMPLIED
+          name  NMTOKENS #IMPLIED
+          arity NMTOKEN  #IMPLIED
+          mark  NMTOKEN  #IMPLIED
+         meta  CDATA    #IMPLIED
 >
 
-<!ELEMENT Abbr %term;>
+<!ELEMENT Abbr %terms;>
 <!ATTLIST Abbr
-          name CDATA #IMPLIED
+          name  NMTOKENS #IMPLIED
+          arity NMTOKEN  #IMPLIED
+          mark  NMTOKEN  #IMPLIED
+         meta  CDATA    #IMPLIED
 >
 
 <!ELEMENT Void EMPTY>
 <!ATTLIST Void
-          name CDATA #IMPLIED
+          name  NMTOKENS #IMPLIED
+          arity NMTOKEN  #IMPLIED
+         mark  NMTOKEN  #IMPLIED
+         meta  CDATA    #IMPLIED
 >
 
 <!-- ENVIRONMENT ENTRIES -->
 
-<!ENTITY % entry '(ABST|ABBR|VOID)'> 
+<!ENTITY % entity '(ABST|ABBR)'> 
 
 <!ELEMENT ABST %term;>
 <!ATTLIST ABST
-          uri  CDATA #REQUIRED
-          name CDATA #IMPLIED
+          uri  CDATA   #REQUIRED
+          name NMTOKEN #IMPLIED
+          mark NMTOKEN #IMPLIED
+         meta CDATA   #IMPLIED
 >
 
 <!ELEMENT ABBR %term;>
 <!ATTLIST ABBR
-          uri  CDATA #REQUIRED
-          name CDATA #IMPLIED
+          uri  CDATA   #REQUIRED
+          name NMTOKEN #IMPLIED
+          mark NMTOKEN #IMPLIED
+         meta CDATA   #IMPLIED
 >
 
-<!ELEMENT VOID EMPTY>
-<!ATTLIST VOID
-          uri  CDATA #REQUIRED
-          name CDATA #IMPLIED
+<!ELEMENT ENTITY %entity;>
+<!ATTLIST ENTITY
+          hierarchy NMTOKEN  #REQUIRED
+          options   NMTOKENS #IMPLIED
 >
 
-<!-- ROOT -->
+<!-- CONVERSION CONSTRAINT SYSTEM -->
 
-<!ELEMENT ENTRY %entry;>
-<!ATTLIST ENTRY
-          hierarchy NMTOKEN  #REQUIRED
-          options   NMTOKENS #IMPLIED
+<!ENTITY % ccs '(ToInfinity)'> 
+
+<!ELEMENT ToInfinity EMPTY>
+<!ATTLIST ToInfinity
+          arity NMTOKEN  #IMPLIED
+          mark  NMTOKENS #IMPLIED
+>
+
+<!ELEMENT CCS %ccs;>
+<!ATTLIST CCS
+          uri  CDATA   #REQUIRED
 >