Conjectures and Hypotheses inside every conjecture and in the sequents now

[helm.git] / helm / style / mmlextension.xsl

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 7aeec143f15f8a2cf3b11cbb934ae7aa900fee91..6ab6ffe1fcfbc51f201b94adcee89a14ff22d278 100644 (file)
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -181,12 +181,12 @@ which generates the toplevel element (see for instance xlink) -->
       <xsl:for-each select="Conjecture">
       <m:mtr>
        <m:mtd>
-        <m:mrow>
+        <m:mrow helm:xref="{@helm:xref}">
          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
          <xsl:for-each select="Decl|Def|Hidden">
           <xsl:choose>
            <xsl:when test="name(.)='Decl'">
-            <m:mrow>
+            <m:mrow helm:xref="{@helm:xref}">
              <xsl:choose>
               <xsl:when test="@name">
                <m:mi><xsl:value-of select="@name"/></m:mi>
@@ -200,7 +200,7 @@ which generates the toplevel element (see for instance xlink) -->
             </m:mrow>
            </xsl:when>
            <xsl:when test="name(.)='Def'">
-            <m:mrow>
+            <m:mrow helm:xref="{@helm:xref}">
              <xsl:choose>
               <xsl:when test="@name">
                <m:mi><xsl:value-of select="@name"/></m:mi>
@@ -214,7 +214,7 @@ which generates the toplevel element (see for instance xlink) -->
             </m:mrow>
            </xsl:when>
            <xsl:otherwise>
-            <m:mrow>
+            <m:mrow helm:xref="{@helm:xref}">
              <m:mi>_</m:mi>
              <m:mo>:?</m:mo>
              <m:mi>_</m:mi>
@@ -424,7 +424,7 @@ which generates the toplevel element (see for instance xlink) -->
       <xsl:for-each select="Decl|Def">
        <m:mtr>
         <m:mtd>
-         <m:mrow>
+         <m:mrow helm:xref="{@helm:xref}">
           <m:mi><xsl:value-of select="@name"/></m:mi>
           <xsl:choose>
            <xsl:when test="name(.) = 'Decl'">