]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/www/lambdadelta/xml/ld.dtd
- helena: the improved attribute system allows to export the sorts of Pi's
[helm.git] / helm / www / lambdadelta / xml / ld.dtd
index 4cb01e225959b5b02b064a1c1e01feb418684734..a6bb14c8850a7e603048648f9981a358101dc050 100644 (file)
@@ -6,11 +6,11 @@
 
 <!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
 
 <!ELEMENT GRef EMPTY>
 <!ATTLIST GRef
-          uri  CDATA   #REQUIRED
-          name NMTOKEN #IMPLIED
+          uri      CDATA   #REQUIRED
+          position NMTOKEN #REQUIRED
+          name     NMTOKEN #IMPLIED
 >
 
 <!ELEMENT Cast %term;>
 <!ATTLIST Cast
 >
 
-<!ELEMENT Appl %terms;>
+<!ELEMENT Appl %term;>
 <!ATTLIST Appl
 >
 
-<!ELEMENT Abst %terms;>
+<!ELEMENT Proj %nodes;>
+<!ATTLIST Proj
+>
+
+<!ELEMENT Abst %term;>
 <!ATTLIST Abst
-          level NMTOKEN #IMPLIED
-         name  NMTOKEN #IMPLIED
+          level    NMTOKEN #IMPLIED
+          position NMTOKEN #REQUIRED
+         name     NMTOKEN #IMPLIED
 >
 
-<!ELEMENT Abbr %terms;>
+<!ELEMENT Abbr %term;>
 <!ATTLIST Abbr
           name  NMTOKEN #IMPLIED
 >
 
 <!ELEMENT GDec %term;>
 <!ATTLIST GDec
-          uri   CDATA    #REQUIRED
-          name  NMTOKEN  #IMPLIED
-         meta  NMTOKENS #IMPLIED
-         lang  NMTOKEN  "en-US"
-         info  CDATA    #IMPLIED
+          uri      CDATA    #REQUIRED
+          position NMTOKEN  #REQUIRED
+          name     NMTOKEN  #IMPLIED
+         meta     NMTOKENS #IMPLIED
+         lang     NMTOKEN  "en-US"
+         info     CDATA    #IMPLIED
 >
 
 <!ELEMENT GDef %term;>
 <!ATTLIST GDef
-          uri  CDATA    #REQUIRED
-          name NMTOKEN  #IMPLIED
-         meta NMTOKENS #IMPLIED
-         lang NMTOKEN  "en-US"
-         info CDATA    #IMPLIED
+          uri      CDATA    #REQUIRED
+          position NMTOKEN  #REQUIRED
+          name     NMTOKEN  #IMPLIED
+         meta     NMTOKENS #IMPLIED
+         lang     NMTOKEN  "en-US"
+         info     CDATA    #IMPLIED
 >
 
 <!ELEMENT ENTITY %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
-          xmlns CDATA #FIXED    "http://lambdadelta.info/"
-          uri   CDATA #REQUIRED
->