Declaration and Definition renamed to Decl and Def because

Definition was already defined in the DTD.

diff --git a/helm/dtd/cic.dtd b/helm/dtd/cic.dtd
index 0a90d9e908fe367780af3bfc0a7d2b418ccca933..a2156a522b507c96a92adf72d9f2605c99a49681 100644 (file)
--- a/helm/dtd/cic.dtd
+++ b/helm/dtd/cic.dtd
@@ -74,6 +74,10 @@
           name CDATA #REQUIRED
           id   ID    #REQUIRED>
 
+<!ELEMENT Sequent ((Decl|Def)*,Goal)>
+<!ATTLIST Sequent
+          id   ID    #REQUIRED>
+
 <!-- Elements used in CIC objects, which are not terms: -->
 
 <!ELEMENT InductiveType (arity,Constructor*)>
@@ -89,6 +93,16 @@
 <!ATTLIST Constructor
           name CDATA #REQUIRED>
 
+<!ELEMENT Decl %term;>
+<!ATTLIST Decl
+          name CDATA #REQUIRED>
+
+<!ELEMENT Def %term;>
+<!ATTLIST Def
+          name CDATA #REQUIRED>
+
+<!ELEMENT Goal %term;>
+
 <!-- CIC terms: -->
 
 <!ELEMENT LAMBDA (source,target)>

diff --git a/helm/dtd/cicobject.dtd b/helm/dtd/cicobject.dtd
index 9514103e45339159e9a2aa7a11db719a2a660879..d78251c1d99b25c2dc1ef7745aa6ee66a3cd783f 100644 (file)
--- a/helm/dtd/cicobject.dtd
+++ b/helm/dtd/cicobject.dtd
@@ -67,6 +67,10 @@
           name CDATA #REQUIRED
           xmlns:m    CDATA      #REQUIRED>
 
+<!ELEMENT Sequent ((Decl|Def)*,Goal)>
+<!ATTLIST Sequent
+          id   ID    #REQUIRED>
+
 <!-- Elements used in CIC objects, which are not terms: -->
 
 <!ELEMENT InductiveType (arity,Constructor*)>
@@ -88,6 +92,16 @@
 
 <!ELEMENT Params (#PCDATA)*>
 
+<!ELEMENT Decl %term;>
+<!ATTLIST Decl
+          name CDATA #REQUIRED>
+
+<!ELEMENT Def %term;>
+<!ATTLIST Def
+          name CDATA #REQUIRED>
+
+<!ELEMENT Goal %term;>
+
 <!-- Sintactic sugar for CIC objects: -->
 
 <!ELEMENT type  %term;>

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 65a2b4612f01e90d00ffcadd01d3261bc50e3a81..6e766e3528c6ecf705b849896e854901a839d1c4 100644 (file)
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -365,7 +365,7 @@ which generates the toplevel element (see for instance xlink) -->
 
 <xsl:template match="Sequent">
  <xsl:variable name="rowlines">
-  <xsl:for-each select="Declaration|Definition">
+  <xsl:for-each select="Decl|Def">
    <xsl:if test="position() != last()">
     <xsl:text>none </xsl:text>
    </xsl:if>
@@ -374,13 +374,13 @@ which generates the toplevel element (see for instance xlink) -->
  </xsl:variable>
     <m:math>
      <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}" rowlines="{$rowlines}">
-      <xsl:for-each select="Declaration|Definition">
+      <xsl:for-each select="Decl|Def">
        <m:mtr>
         <m:mtd>
          <m:mrow>
           <m:mi><xsl:value-of select="@name"/></m:mi>
           <xsl:choose>
-           <xsl:when test="name(.) = 'Declaration'">
+           <xsl:when test="name(.) = 'Decl'">
             <m:mo>:</m:mo>
            </xsl:when>
            <xsl:otherwise>
@@ -392,7 +392,7 @@ which generates the toplevel element (see for instance xlink) -->
         </m:mtd>
        </m:mtr>
       </xsl:for-each>
-      <xsl:if test="not(Declaration|Definition)">
+      <xsl:if test="not(Decl|Def)">
       <m:mtr>
        <m:mtd>
         <m:mrow>

diff --git a/helm/style/objcontent.xsl b/helm/style/objcontent.xsl
index aef9daa6b666828280ec4a2b6bf1b8302c37f74b..898e41a985e448066d0c053df8656068ac47799f 100644 (file)
--- a/helm/style/objcontent.xsl
+++ b/helm/style/objcontent.xsl
@@ -56,7 +56,7 @@
 
 <xsl:template match="Sequent">  <!-- For Sequents there are no annotations --> 
     <Sequent helm:xref="{@id}">
-     <xsl:for-each select="Declaration|Definition">
+     <xsl:for-each select="Decl|Def">
       <xsl:copy>
        <xsl:attribute name="name">
         <xsl:value-of select="@name"/>