From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 10 Apr 2003 17:11:46 +0000 (+0000)
Subject: NuPrlDefinition element handling added
X-Git-Tag: before_refactoring~23
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4772f0cc5107b3809128e8ed0bbef4bfffbfe1ff;p=helm.git

NuPrlDefinition element handling added
---

diff --git a/helm/nuprl_stylesheets/nuprl_content_to_html2.xsl b/helm/nuprl_stylesheets/nuprl_content_to_html2.xsl
index 43d420f2f..cc6e7c9cc 100644
--- a/helm/nuprl_stylesheets/nuprl_content_to_html2.xsl
+++ b/helm/nuprl_stylesheets/nuprl_content_to_html2.xsl
@@ -2844,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">
diff --git a/helm/nuprl_stylesheets/nuprl_mmlextension.xsl b/helm/nuprl_stylesheets/nuprl_mmlextension.xsl
index 028579230..f6c1590df 100644
--- a/helm/nuprl_stylesheets/nuprl_mmlextension.xsl
+++ b/helm/nuprl_stylesheets/nuprl_mmlextension.xsl
@@ -251,6 +251,18 @@ which generates the toplevel element (see for instance xlink) -->
 </xsl:template>
 
 
+<!-- NuPRLDefinition -->
+
+<xsl:template match="NuPrlDefinition">
+ <m:math>
+  <m:mrow>
+   <xsl:apply-templates select="*[1]"/>
+   <m:mo> := </m:mo>
+   <xsl:apply-templates select="*[2]"/>
+  </m:mrow>
+ </m:math>
+</xsl:template>
+
 <!-- DEFINITION -->
 
 <xsl:template match="Definition">
diff --git a/helm/nuprl_stylesheets/nuprl_proof.xsl b/helm/nuprl_stylesheets/nuprl_proof.xsl
index f6eb2a7c0..b699ed402 100644
--- a/helm/nuprl_stylesheets/nuprl_proof.xsl
+++ b/helm/nuprl_stylesheets/nuprl_proof.xsl
@@ -15,6 +15,12 @@
   </Definition>
 </xsl:template>
 
+<xsl:template match="NuPrlDefinition">
+ <NuPrlDefinition>
+  <xsl:apply-templates select="*"/>
+ </NuPrlDefinition>
+</xsl:template>
+
 <xsl:template match="node">
   <xsl:element name="Node">
     <xsl:apply-templates/>