Conjectures and Hypotheses inside every conjecture and in the sequents now

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

diff --git a/helm/style/objcontent.xsl b/helm/style/objcontent.xsl
index 5b375084b970625caa0438663a7dc1040d1982ba..b4a0e748da859eb07d2a95f493c8a8ecbabe3ce3 100644 (file)
--- a/helm/style/objcontent.xsl
+++ b/helm/style/objcontent.xsl
@@ -61,6 +61,9 @@
        <xsl:attribute name="name">
         <xsl:value-of select="@name"/>
        </xsl:attribute>
+       <xsl:attribute name="helm-xref">
+        <xsl:value-of select="@id"/>
+       </xsl:attribute>
        <xsl:apply-templates select="*[1]"/>
       </xsl:copy>
      </xsl:for-each>
@@ -114,10 +117,13 @@
 <xsl:template match="CurrentProof" mode="noannot">
     <CurrentProof name="{@name}" helm:xref="{@id}">
      <xsl:for-each select="Conjecture">
-      <Conjecture no="{@no}">
+      <Conjecture no="{@no}" helm:xref="{@id}">
         <xsl:for-each select="*">
          <xsl:copy>
-          <xsl:copy-of select="@*"/>
+          <xsl:copy-of select="@name"/>
+          <xsl:attribute name="helm:xref">
+           <xsl:value-of select="@id"/>
+          </xsl:attribute>
           <xsl:apply-templates select="*"/>
          </xsl:copy>
         </xsl:for-each>