<!-- CIC OBJECTS -->
+<xsl:template match="Sequent"> <!-- For Sequents there are no annotations -->
+ <Sequent helm:xref="{@id}" no="{@no}">
+ <xsl:for-each select="Decl|Def|Hidden">
+ <xsl:copy>
+ <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>
+ <Goal>
+ <xsl:apply-templates select="Goal/*[1]"/>
+ </Goal>
+ </Sequent>
+</xsl:template>
+
<xsl:template match="Definition" mode="noannot">
<Definition name="{@name}" helm:xref="{@id}">
<xsl:if test="string(@params) != """>
<xsl:template match="CurrentProof" mode="noannot">
<CurrentProof name="{@name}" helm:xref="{@id}">
<xsl:for-each select="Conjecture">
- <Conjecture no="./{@no}">
- <xsl:apply-templates select="."/>
+ <Conjecture no="{@no}" helm:xref="{@id}">
+ <xsl:for-each select="*">
+ <xsl:copy>
+ <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>
</Conjecture>
</xsl:for-each>
<body>