X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fnuprl_stylesheets%2Fnuprl_content_to_html2.xsl;h=cc6e7c9cccee494274d07c21d7c12875924af0f7;hb=d3c72d6856cd185e5b3e9f2e8b928b78c7031ed1;hp=5fb0c0d8aaec85dd4059d28f78543bfac4629bdb;hpb=e9db2c226034b75e69dba72b6bd577a7bcf6a31f;p=helm.git

diff --git a/helm/nuprl_stylesheets/nuprl_content_to_html2.xsl b/helm/nuprl_stylesheets/nuprl_content_to_html2.xsl
index 5fb0c0d8a..cc6e7c9cc 100644
--- a/helm/nuprl_stylesheets/nuprl_content_to_html2.xsl
+++ b/helm/nuprl_stylesheets/nuprl_content_to_html2.xsl
@@ -2785,10 +2785,6 @@
           </xsl:call-template>
           <xsl:text>By </xsl:text>
           <xsl:apply-templates select="TacticInstance/@name"/>
-          <!-- CSC: extra_info in HTML to be rendered here -->
-          <xsl:for-each select="TacticInstance/extra_info">
-           <xsl:copy-of select="*|text()"/>
-          </xsl:for-each>
           <a style="text-decoration:underline ; color:green" href="{TacticInstance/@uri}">Tactic Details</a>
           <xsl:if test="$explode_tactics">
 	   <span ID="{$freshid4}">
@@ -2848,6 +2844,14 @@
 	  </xsl:if>
 </xsl:template>
 
+<!-- NuPRLDefinition -->
+
+<xsl:template match="NuPrlDefinition">
+ <xsl:apply-templates select="*[1]"/>
+ <xsl:text> := </xsl:text>
+ <xsl:apply-templates select="*[2]"/>
+</xsl:template>
+
 <!-- DEFINITION -->
 
 <xsl:template match="Definition">