X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fxml%2Fld.dtd;h=d97173d8279fb5202bef9542f2998f1a3abadc6b;hb=f7988fc51f7c96617aa2b3320628645480af681a;hp=83cfc0596e0e8fdf96ce1d47859c482f3a5f5241;hpb=3f6af93003bef461be59c8d4c96009c631f0c2e7;p=helm.git

diff --git a/helm/software/lambda-delta/xml/ld.dtd b/helm/software/lambda-delta/xml/ld.dtd
index 83cfc0596..d97173d82 100644
--- a/helm/software/lambda-delta/xml/ld.dtd
+++ b/helm/software/lambda-delta/xml/ld.dtd
@@ -10,55 +10,69 @@
 
 <!ENTITY % term '(%node;*,%leaf;)'>
 
+<!ENTITY % terms '(%term;*)'>
+
 <!ELEMENT Sort EMPTY>
 <!ATTLIST Sort
-          position NMTOKEN  #REQUIRED
-          name     NMTOKENS #IMPLIED
-          mark     NMTOKENS #IMPLIED
+          position NMTOKEN #REQUIRED
+          name     NMTOKEN #IMPLIED
+          mark     NMTOKEN #IMPLIED
+	  meta     CDATA   #IMPLIED
 >
 
 <!ELEMENT LRef EMPTY>
 <!ATTLIST LRef
-          position NMTOKEN  #REQUIRED
-          name     NMTOKENS #IMPLIED
-          mark     NMTOKENS #IMPLIED
+          position NMTOKEN #REQUIRED
+	  offset   NMTOKEN #IMPLIED
+          name     NMTOKEN #IMPLIED
+          mark     NMTOKEN #IMPLIED
+	  meta     CDATA   #IMPLIED
 >
 
 <!ELEMENT GRef EMPTY>
 <!ATTLIST GRef
-          uri  CDATA    #REQUIRED
-          name NMTOKENS #IMPLIED
-          mark NMTOKENS #IMPLIED
+          uri  CDATA   #REQUIRED
+          name NMTOKEN #IMPLIED
+          mark NMTOKEN #IMPLIED
+	  meta CDATA   #IMPLIED
 >
 
 <!ELEMENT Cast %term;>
 <!ATTLIST Cast
-          name NMTOKENS #IMPLIED
-          mark NMTOKENS #IMPLIED
+          arity NMTOKEN #IMPLIED
+          mark  NMTOKEN #IMPLIED
+	  meta  CDATA   #IMPLIED
 >
 
-<!ELEMENT Appl %term;>
+<!ELEMENT Appl %terms;>
 <!ATTLIST Appl
-          name NMTOKENS #IMPLIED
-          mark NMTOKENS #IMPLIED
+          arity NMTOKEN #IMPLIED
+          mark  NMTOKEN #IMPLIED
+	  meta  CDATA   #IMPLIED
 >
 
-<!ELEMENT Abst %term;>
+<!ELEMENT Abst %terms;>
 <!ATTLIST Abst
-          name NMTOKENS #IMPLIED
-          mark NMTOKENS #IMPLIED
+          name  NMTOKENS #IMPLIED
+          arity NMTOKEN  #IMPLIED
+          mark  NMTOKEN  #IMPLIED
+	  meta  CDATA    #IMPLIED
 >
 
-<!ELEMENT Abbr %term;>
+<!ELEMENT Abbr %terms;>
 <!ATTLIST Abbr
-          name NMTOKENS #IMPLIED
-          mark NMTOKENS #IMPLIED
+          name  NMTOKENS #IMPLIED
+          arity NMTOKEN  #IMPLIED
+          mark  NMTOKEN  #IMPLIED
+	  meta  CDATA    #IMPLIED
 >
 
 <!ELEMENT Void EMPTY>
 <!ATTLIST Void
-          name NMTOKENS #IMPLIED
-          mark NMTOKENS #IMPLIED
+          name  NMTOKENS #IMPLIED
+          arity NMTOKEN  #IMPLIED
+	  mark  NMTOKEN  #IMPLIED
+	  meta  CDATA    #IMPLIED
 >
 
 <!-- ENVIRONMENT ENTRIES -->
@@ -67,22 +81,37 @@
 
 <!ELEMENT ABST %term;>
 <!ATTLIST ABST
-          uri  CDATA    #REQUIRED
-          name NMTOKENS #IMPLIED
-          mark NMTOKENS #IMPLIED
+          uri  CDATA   #REQUIRED
+          name NMTOKEN #IMPLIED
+          mark NMTOKEN #IMPLIED
+	  meta CDATA   #IMPLIED
 >
 
 <!ELEMENT ABBR %term;>
 <!ATTLIST ABBR
-          uri  CDATA    #REQUIRED
-          name NMTOKENS #IMPLIED
-          mark NMTOKENS #IMPLIED
+          uri  CDATA   #REQUIRED
+          name NMTOKEN #IMPLIED
+          mark NMTOKEN #IMPLIED
+	  meta CDATA   #IMPLIED
 >
 
-<!-- ROOT -->
-
 <!ELEMENT ENTITY %entity;>
 <!ATTLIST ENTITY
           hierarchy NMTOKEN  #REQUIRED
           options   NMTOKENS #IMPLIED
 >
+
+<!-- CONVERSION CONSTRAINT SYSTEM -->
+
+<!ENTITY % ccs '(ToInfinity)'> 
+
+<!ELEMENT ToInfinity EMPTY>
+<!ATTLIST ToInfinity
+          arity NMTOKEN  #IMPLIED
+          mark  NMTOKENS #IMPLIED
+>
+
+<!ELEMENT CCS %ccs;>
+<!ATTLIST CCS
+          uri  CDATA   #REQUIRED
+>