X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fxml%2Fld.dtd;h=0fb547e45bf00fbc2557662ca92ebb488f9c65a2;hb=58ddc56896384e0a1e8a7d331aae9eded8510c70;hp=369f8c400ba593ebf60ea0342686aed977efcf04;hpb=2a5e0b799cd6aae5d920c67a5ddc9d9888cf7e80;p=helm.git

diff --git a/helm/www/lambdadelta/xml/ld.dtd b/helm/www/lambdadelta/xml/ld.dtd
index 369f8c400..0fb547e45 100644
--- a/helm/www/lambdadelta/xml/ld.dtd
+++ b/helm/www/lambdadelta/xml/ld.dtd
@@ -6,135 +6,87 @@
 
 <!ENTITY % leaf '(Sort|LRef|GRef)'>
 
-<!ENTITY % node '(Cast|Appl|Abst|Abbr|Void)'>
+<!ENTITY % node '(Proj|Cast|Appl|Abst|Abbr|Void)'>
 
 <!ENTITY % term '(%node;*,%leaf;)'>
 
-<!ENTITY % terms '(%term;*)'>
+<!ENTITY % nodes '(%node;*)'>
 
 <!ELEMENT Sort EMPTY>
 <!ATTLIST Sort
           position NMTOKEN #REQUIRED
           name     NMTOKEN #IMPLIED
-          mark     NMTOKEN #IMPLIED
-	  meta     CDATA   #IMPLIED
 >
 
 <!ELEMENT LRef EMPTY>
 <!ATTLIST LRef
           position NMTOKEN #REQUIRED
-	  offset   NMTOKEN #IMPLIED
           name     NMTOKEN #IMPLIED
-          mark     NMTOKEN #IMPLIED
-	  meta     CDATA   #IMPLIED
 >
 
 <!ELEMENT GRef EMPTY>
 <!ATTLIST GRef
-          uri  CDATA   #REQUIRED
-          name NMTOKEN #IMPLIED
-          mark NMTOKEN #IMPLIED
-	  meta CDATA   #IMPLIED
+          uri      CDATA   #REQUIRED
+          position NMTOKEN #REQUIRED
+          name     NMTOKEN #IMPLIED
 >
 
 <!ELEMENT Cast %term;>
 <!ATTLIST Cast
-          arity NMTOKEN #IMPLIED
-          mark  NMTOKEN #IMPLIED
-	  meta  CDATA   #IMPLIED
 >
 
-<!ELEMENT Appl %terms;>
+<!ELEMENT Appl %term;>
 <!ATTLIST Appl
-          arity NMTOKEN #IMPLIED
-          mark  NMTOKEN #IMPLIED
-	  meta  CDATA   #IMPLIED
 >
 
-<!ELEMENT Abst %terms;>
+<!ELEMENT Proj %nodes;>
+<!ATTLIST Proj
+>
+
+<!ELEMENT Abst %term;>
 <!ATTLIST Abst
-          level NMTOKEN  #IMPLIED
-	  name  NMTOKENS #IMPLIED
-          arity NMTOKEN  #IMPLIED
-          mark  NMTOKEN  #IMPLIED
-	  meta  CDATA    #IMPLIED
+          layer    NMTOKEN #IMPLIED
+          position NMTOKEN #REQUIRED
+	  name     NMTOKEN #IMPLIED
 >
 
-<!ELEMENT Abbr %terms;>
+<!ELEMENT Abbr %term;>
 <!ATTLIST Abbr
-          name  NMTOKENS #IMPLIED
-          arity NMTOKEN  #IMPLIED
-          mark  NMTOKEN  #IMPLIED
-	  meta  CDATA    #IMPLIED
+          name  NMTOKEN #IMPLIED
 >
 
 <!ELEMENT Void EMPTY>
 <!ATTLIST Void
-          name  NMTOKENS #IMPLIED
-          arity NMTOKEN  #IMPLIED
-	  mark  NMTOKEN  #IMPLIED
-	  meta  CDATA    #IMPLIED
+          name  NMTOKEN #IMPLIED
 >
 
 <!-- ENVIRONMENT ENTRIES -->
 
-<!ENTITY % entity '(ABST|ABBR)'> 
-
-<!ELEMENT ABST %term;>
-<!ATTLIST ABST
-          uri   CDATA    #REQUIRED
-          level NMTOKEN  #IMPLIED
-          name  NMTOKEN  #IMPLIED
-          mark  NMTOKEN  #IMPLIED
-	  meta  NMTOKENS #IMPLIED
-	  lang  NMTOKEN  "en-US"
-	  info  CDATA    #IMPLIED
+<!ENTITY % constant '(GDec|GDef)'> 
+
+<!ELEMENT GDec %term;>
+<!ATTLIST GDec
+          uri      CDATA    #REQUIRED
+          position NMTOKEN  #REQUIRED
+          name     NMTOKEN  #IMPLIED
+	  meta     NMTOKENS #IMPLIED
+	  lang     NMTOKEN  "en-US"
+	  info     CDATA    #IMPLIED
 >
 
-<!ELEMENT ABBR %term;>
-<!ATTLIST ABBR
-          uri  CDATA    #REQUIRED
-          name NMTOKEN  #IMPLIED
-          mark NMTOKEN  #IMPLIED
-	  meta NMTOKENS #IMPLIED
-	  lang NMTOKEN  "en-US"
-	  info CDATA    #IMPLIED
+<!ELEMENT GDef %term;>
+<!ATTLIST GDef
+          uri      CDATA    #REQUIRED
+          position NMTOKEN  #REQUIRED
+          name     NMTOKEN  #IMPLIED
+	  meta     NMTOKENS #IMPLIED
+	  lang     NMTOKEN  "en-US"
+	  info     CDATA    #IMPLIED
 >
 
-<!ELEMENT ENTITY %entity;>
-<!ATTLIST ENTITY
-          xmlns     CDATA    #FIXED    "http://lambdadelta.info"
+<!ELEMENT CONSTANT %constant;>
+<!ATTLIST CONSTANT
+          xmlns     CDATA    #FIXED    "http://lambdadelta.info/"
 	  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
-          xmlns CDATA #FIXED    "http://lambdadelta.info"
-          uri   CDATA #REQUIRED
->