From: Irene Schena <irene.schena@unibo.it>
Date: Fri, 26 Jan 2001 14:10:50 +0000 (+0000)
Subject: Modified Files:
X-Git-Tag: no-uwobo~7
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7ab23379f84c1b1b999a359830d333fc2925bb58;p=helm.git

Modified Files:
1) mmlextension.xsl: <m:mo helm:xref="m:in/@helm:xref"> lacks {} !
2) reals.xsl: added definitionURL and helm:xref to the limit (limit1_in)
and moved helm:xref into <m:minus> of Rinv.con
---

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 5537076fb..a22dc0dd3 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -1266,9 +1266,7 @@
      <m:mtr>
       <m:mtd>
        <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
-       <m:mo helm:xref="m:in/@helm:xref"> 
-        =
-       </m:mo>
+       <m:mo helm:xref="{m:in/@helm:xref}">=</m:mo>
        <xsl:apply-templates select="."/>
       </m:mtd>
      </m:mtr>
diff --git a/helm/style/reals.xsl b/helm/style/reals.xsl
index 45ed5f61c..7a1a0d183 100644
--- a/helm/style/reals.xsl
+++ b/helm/style/reals.xsl
@@ -121,10 +121,10 @@
          <xsl:attribute name="definitionURL">
           <xsl:value-of select="CONST/@uri"/> 
          </xsl:attribute>
+         <xsl:attribute name="helm:xref">
+          <xsl:value-of select="CONST/@id"/>
+         </xsl:attribute>
         </m:minus>
-        <xsl:attribute name="helm:xref">
-         <xsl:value-of select="CONST/@id"/>
-        </xsl:attribute>
         <m:cn>1</m:cn>
        </m:apply>
       </m:apply>
@@ -231,7 +231,14 @@
         </xsl:when>
         <xsl:otherwise>
          <m:apply helm:xref="{@id}">
-          <m:limit/>
+          <m:limit>
+            <xsl:attribute name="definitionURL">
+             <xsl:value-of select="CONST/@uri"/> 
+            </xsl:attribute>
+            <xsl:attribute name="helm:xref">
+             <xsl:value-of select="CONST/@id"/>
+            </xsl:attribute>
+           </m:limit>
           <m:bvar>
            <m:ci>$x</m:ci>
           </m:bvar>
@@ -266,7 +273,7 @@
        <xsl:choose>
         <xsl:when test="name(*[2]) = 'LAMBDA'">
          <m:apply helm:xref="{@id}">
-          <m:diff >
+          <m:diff>
            <xsl:attribute name="definitionURL">
             <xsl:value-of select="CONST/@uri"/> 
            </xsl:attribute>
@@ -304,3 +311,5 @@
 </xsl:template>
 
 </xsl:stylesheet>
+
+