X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fxml%2Fld.dtd;h=0378bb3979eae401c68cbe36a11bb8e408011cb9;hb=513c7211bb07abd4c1da842a29c05301890aa73a;hp=1a3103c2a3de79316e9e698c32f33167242bea6b;hpb=39b42ed90bc74c8b6293842f1ac4aca60fc0c37e;p=helm.git

diff --git a/helm/software/lambda-delta/xml/ld.dtd b/helm/software/lambda-delta/xml/ld.dtd
index 1a3103c2a..0378bb397 100644
--- a/helm/software/lambda-delta/xml/ld.dtd
+++ b/helm/software/lambda-delta/xml/ld.dtd
@@ -10,6 +10,8 @@
 
 <!ENTITY % term '(%node;*,%leaf;)'>
 
+<!ENTITY % terms '(%term;*)'>
+
 <!ELEMENT Sort EMPTY>
 <!ATTLIST Sort
           position NMTOKEN #REQUIRED
@@ -21,6 +23,7 @@
 <!ELEMENT LRef EMPTY>
 <!ATTLIST LRef
           position NMTOKEN #REQUIRED
+	  offset   NMTOKEN #IMPLIED
           name     NMTOKEN #IMPLIED
           mark     NMTOKEN #IMPLIED
 	  meta     CDATA   #IMPLIED
@@ -41,22 +44,23 @@
 	  meta  CDATA   #IMPLIED
 >
 
-<!ELEMENT Appl %term;>
+<!ELEMENT Appl %terms;>
 <!ATTLIST Appl
           arity NMTOKEN #IMPLIED
           mark  NMTOKEN #IMPLIED
 	  meta  CDATA   #IMPLIED
 >
 
-<!ELEMENT Abst %term;>
+<!ELEMENT Abst %terms;>
 <!ATTLIST Abst
-          name  NMTOKENS #IMPLIED
+          level NMTOKEN  #IMPLIED
+	  name  NMTOKENS #IMPLIED
           arity NMTOKEN  #IMPLIED
           mark  NMTOKEN  #IMPLIED
 	  meta  CDATA    #IMPLIED
 >
 
-<!ELEMENT Abbr %term;>
+<!ELEMENT Abbr %terms;>
 <!ATTLIST Abbr
           name  NMTOKENS #IMPLIED
           arity NMTOKEN  #IMPLIED
@@ -78,10 +82,11 @@
 
 <!ELEMENT ABST %term;>
 <!ATTLIST ABST
-          uri  CDATA   #REQUIRED
-          name NMTOKEN #IMPLIED
-          mark NMTOKEN #IMPLIED
-	  meta CDATA   #IMPLIED
+          uri   CDATA   #REQUIRED
+          level NMTOKEN #IMPLIED
+          name  NMTOKEN #IMPLIED
+          mark  NMTOKEN #IMPLIED
+	  meta  CDATA   #IMPLIED
 >
 
 <!ELEMENT ABBR %term;>
@@ -92,10 +97,38 @@
 	  meta CDATA   #IMPLIED
 >
 
-<!-- ROOT -->
-
 <!ELEMENT ENTITY %entity;>
 <!ATTLIST ENTITY
           hierarchy NMTOKEN  #REQUIRED
           options   NMTOKENS #IMPLIED
 >
+
+<!-- CONVERSION CONSTRAINT SYSTEM -->
+
+<!ENTITY % cc '(ToPositive|ToOne|ToNext)'> 
+
+<!ENTITY % ccs '(%cc;*)'>
+
+<!ELEMENT ToPositive EMPTY>
+<!ATTLIST ToPositive
+          arity NMTOKEN  #IMPLIED
+          mark  NMTOKENS #IMPLIED
+>
+
+<!ELEMENT ToOne EMPTY>
+<!ATTLIST ToOne
+          arity NMTOKEN  #IMPLIED
+          mark  NMTOKENS #IMPLIED
+>
+
+<!ELEMENT ToNext EMPTY>
+<!ATTLIST ToNext
+          arity NMTOKEN  #IMPLIED
+          prec  NMTOKENS #IMPLIED
+          next  NMTOKENS #IMPLIED
+>
+
+<!ELEMENT CCS %ccs;>
+<!ATTLIST CCS
+          uri  CDATA   #REQUIRED
+>