X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fxml%2Fld.dtd;fp=helm%2Fsoftware%2Fhelena%2Fxml%2Fld.dtd;h=3939d6f5b743a041cb701333b1220ebc735e5267;hb=95872555aaa040a22ad2d93cb1278f79e20da70c;hp=0000000000000000000000000000000000000000;hpb=4025c3f5b36025380dcad84bb7a97045d08652f6;p=helm.git

diff --git a/helm/software/helena/xml/ld.dtd b/helm/software/helena/xml/ld.dtd
new file mode 100644
index 000000000..3939d6f5b
--- /dev/null
+++ b/helm/software/helena/xml/ld.dtd
@@ -0,0 +1,140 @@
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!-- DTD for persistent lambda-delta logical data -->
+
+<!-- TERMS -->
+
+<!ENTITY % leaf '(Sort|LRef|GRef)'>
+
+<!ENTITY % node '(Cast|Appl|Abst|Abbr|Void)'>
+
+<!ENTITY % term '(%node;*,%leaf;)'>
+
+<!ENTITY % terms '(%term;*)'>
+
+<!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
+>
+
+<!ELEMENT Cast %term;>
+<!ATTLIST Cast
+          arity NMTOKEN #IMPLIED
+          mark  NMTOKEN #IMPLIED
+	  meta  CDATA   #IMPLIED
+>
+
+<!ELEMENT Appl %terms;>
+<!ATTLIST Appl
+          arity NMTOKEN #IMPLIED
+          mark  NMTOKEN #IMPLIED
+	  meta  CDATA   #IMPLIED
+>
+
+<!ELEMENT Abst %terms;>
+<!ATTLIST Abst
+          level NMTOKEN  #IMPLIED
+	  name  NMTOKENS #IMPLIED
+          arity NMTOKEN  #IMPLIED
+          mark  NMTOKEN  #IMPLIED
+	  meta  CDATA    #IMPLIED
+>
+
+<!ELEMENT Abbr %terms;>
+<!ATTLIST Abbr
+          name  NMTOKENS #IMPLIED
+          arity NMTOKEN  #IMPLIED
+          mark  NMTOKEN  #IMPLIED
+	  meta  CDATA    #IMPLIED
+>
+
+<!ELEMENT Void EMPTY>
+<!ATTLIST Void
+          name  NMTOKENS #IMPLIED
+          arity NMTOKEN  #IMPLIED
+	  mark  NMTOKEN  #IMPLIED
+	  meta  CDATA    #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
+>
+
+<!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 ENTITY %entity;>
+<!ATTLIST ENTITY
+          xmlns     CDATA    #FIXED    "http://lambda-delta.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://lambda-delta.info"
+          uri   CDATA #REQUIRED
+>