X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fstyle%2Freals.xsl;h=7a1a0d1839de749ac5c4e0a23491d0f565f00393;hb=4e8b137b58ec6763785b8ee490ee8cd6cb77b5bf;hp=45ed5f61c2df0e9a8be699b54a61813e4ef9e623;hpb=f079a5948394ada2f2aba69270869058111bb3fe;p=helm.git

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>
+
+