Lambda notazione.

diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index ecc63d53abd33d55de7e85a63a3521ed958b61ad..71a82f613d16be524a61c0eb1c75febbf2e0945f 100644 (file)
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -297,7 +297,132 @@
      <FONT color="red">&#x00a0;hence&#x00a0;</FONT>
      <xsl:apply-templates mode="inline" select="*[7]"/>
     </xsl:when>
-   
+
+       <xsl:when test="$name='subst'">
+       <xsl:apply-templates select="*[3]" mode="inline"/>
+       <xsl:text>[</xsl:text>
+       <xsl:apply-templates select="*[4]" mode="inline"/>
+       <a href="{*[1]/@definitionURL}">
+       <FONT color="green" FACE="symbol">
+        <xsl:text>&#x00ac;</xsl:text>
+       </FONT>
+       </a>
+       <xsl:apply-templates select="*[2]" mode="inline"/>
+       <xsl:text>]</xsl:text>
+      </xsl:when>
+
+      <xsl:when test="$name='lift_with_base'">
+       <SUB>
+       <xsl:apply-templates select="*[3]" mode="inline"/>
+       </SUB>
+       <a href="{*[1]/@definitionURL}">
+       <FONT color="green" FACE="symbol">
+        <xsl:text>&#x00ad;</xsl:text>
+       </FONT>
+       </a>
+       <SUP>
+       <xsl:apply-templates select="*[4]" mode="inline"/>
+       </SUP>
+       <xsl:text>(</xsl:text>
+       <xsl:apply-templates select="*[2]" mode="inline"/>
+       <xsl:text>)</xsl:text>
+      </xsl:when>
+
+      <xsl:when test="$name='lift'">
+       <a href="{*[1]/@definitionURL}">
+       <FONT color="green" FACE="symbol">
+        <xsl:text>&#x00ad;</xsl:text>
+       </FONT>
+       </a>
+       <SUP>
+       <xsl:apply-templates select="*[2]" mode="inline"/>
+       </SUP>
+       <xsl:text>(</xsl:text>
+       <xsl:apply-templates select="*[3]" mode="inline"/>
+       <xsl:text>)</xsl:text>
+      </xsl:when>
+
+      <!-- reduction --> 
+      <xsl:when test="$name='beta_red1'">
+       <xsl:apply-templates select="*[2]" mode="inline"/>
+       <a href="{*[1]/@definitionURL}">
+       <FONT color="green" FACE="symbol">
+        <xsl:text>&#x00ae;</xsl:text>
+       </FONT>
+       <SUB>
+        <FONT color="green" FACE="symbol">
+         <xsl:text>&#x0062;</xsl:text>
+        </FONT>
+       </SUB>
+       </a>
+       <xsl:apply-templates select="*[3]" mode="inline"/>
+      </xsl:when>
+
+      <xsl:when test="$name='beta_red'">
+       <xsl:apply-templates select="*[2]" mode="inline"/>
+       <a href="{*[1]/@definitionURL}">
+       <FONT color="green" FACE="symbol">
+        <xsl:text>&#x00ae;</xsl:text>
+       </FONT>
+       <SUB>
+        <FONT color="green" FACE="symbol">
+         <xsl:text>&#x0062;*</xsl:text>
+        </FONT>
+       </SUB>
+       </a>
+       <xsl:apply-templates select="*[3]" mode="inline"/>
+      </xsl:when>
+
+      <xsl:when test="$name='par_beta_red1'">
+       <xsl:apply-templates select="*[2]" mode="inline"/>
+       <a href="{*[1]/@definitionURL}">
+       <FONT color="green" FACE="symbol">
+        <xsl:text>&#x00de;</xsl:text>
+       </FONT>
+       <SUB>
+        <FONT color="green" FACE="symbol">
+         <xsl:text>&#x0062;</xsl:text>
+        </FONT>
+       </SUB>
+       </a>
+       <xsl:apply-templates select="*[3]" mode="inline"/>
+      </xsl:when>
+
+      <xsl:when test="$name='par_beta_red'">
+       <xsl:apply-templates select="*[2]" mode="inline"/>
+       <a href="{*[1]/@definitionURL}">
+       <FONT color="green" FACE="symbol">
+        <xsl:text>&#x00de;</xsl:text>
+       </FONT>
+       <SUB>
+        <FONT color="green" FACE="symbol">
+         <xsl:text>&#x0062;*</xsl:text>
+        </FONT>
+       </SUB>
+       </a>
+       <xsl:apply-templates select="*[3]" mode="inline"/>
+      </xsl:when>
+
+      <!-- forgetful -->
+      <xsl:when test="$name='forgetful'">
+       <a href="{*[1]/@definitionURL}">|</a>
+       <xsl:apply-templates select="*[2]" mode="inline"/>
+       <a href="{*[1]/@definitionURL}">|</a>
+      </xsl:when>
+ 
+      <!-- boolean algebra of redexes -->
+
+      <!-- isomorphic -->
+      <xsl:when test="$name='isomorphic'">
+       <xsl:apply-templates select="*[2]" mode="inline"/>
+       <a href="{*[1]/@definitionURL}">
+        <FONT color="green" FACE="symbol">
+        <xsl:text>&#x0040;</xsl:text>
+       </FONT>
+       </a>
+       <xsl:apply-templates select="*[3]" mode="inline"/>
+      </xsl:when>
+
       <!-- INTERP -->
       <xsl:when test="$name='interp'">
          <font color="green">[</font>
@@ -1061,6 +1186,133 @@
         <xsl:with-param name="current_indent" select="$current_indent"/>
        </xsl:apply-templates>
       </xsl:when>
+      <!-- ***************************************** -->
+      <!-- *********** LAMBDA ELEMENTS ************** -->
+      <!-- ***************************************** -->
+      <xsl:when test="$name='subst'">
+       <xsl:apply-templates select="*[2]"/>
+       <xsl:text>[</xsl:text>
+       <xsl:apply-templates select="*[4]"/>
+       <a href="{*[1]/@definitionURL}">
+       <FONT color="blue" SIZE="+0" FACE="symbol">
+        <xsl:text>&#x00ac;</xsl:text>
+       </FONT>
+       </a>
+       <xsl:apply-templates select="*[3]"/>
+       <xsl:text>]</xsl:text>
+      </xsl:when>
+
+      <xsl:when test="$name='lift_with_base'">
+       <SUB>
+       <xsl:apply-templates select="*[3]" mode="inline"/>
+       </SUB>
+       <a href="{*[1]/@definitionURL}">
+       <FONT color="green" FACE="symbol">
+        <xsl:text>&#x00ad;</xsl:text>
+       </FONT>
+       </a>
+       <SUP>
+       <xsl:apply-templates select="*[4]" mode="inline"/>
+       </SUP>
+       <xsl:text>(</xsl:text>
+       <xsl:apply-templates select="*[2]" mode="inline"/>
+       <xsl:text>)</xsl:text>
+      </xsl:when>
+
+      <xsl:when test="$name='lift'">
+       <a href="{*[1]/@definitionURL}">
+       <FONT color="green" FACE="symbol">
+        <xsl:text>&#x00ad;</xsl:text>
+       </FONT>
+       </a>
+       <SUP>
+       <xsl:apply-templates select="*[2]" mode="inline"/>
+       </SUP>
+       <xsl:text>(</xsl:text>
+       <xsl:apply-templates select="*[3]" mode="inline"/>
+       <xsl:text>)</xsl:text>
+      </xsl:when>
+
+      <!-- reduction --> 
+      <xsl:when test="$name='beta_red1'">
+       <xsl:apply-templates select="*[2]" mode="inline"/>
+       <a href="{*[1]/@definitionURL}">
+       <FONT color="green" FACE="symbol">
+        <xsl:text>&#x00ae;</xsl:text>
+       </FONT>
+       <SUB>
+        <FONT color="green" FACE="symbol">
+         <xsl:text>&#x0062;</xsl:text>
+        </FONT>
+       </SUB>
+       </a>
+       <xsl:apply-templates select="*[3]" mode="inline"/>
+      </xsl:when>
+ 
+      <xsl:when test="$name='beta_red'">
+       <xsl:apply-templates select="*[2]" mode="inline"/>
+       <a href="{*[1]/@definitionURL}">
+       <FONT color="green" FACE="symbol">
+        <xsl:text>&#x00ae;</xsl:text>
+       </FONT>
+       <SUB>
+        <FONT color="green" FACE="symbol">
+         <xsl:text>&#x0062;*</xsl:text>
+        </FONT>
+       </SUB>
+       </a>
+       <xsl:apply-templates select="*[3]" mode="inline"/>
+      </xsl:when>
+
+      <xsl:when test="$name='par_beta_red1'">
+       <xsl:apply-templates select="*[2]" mode="inline"/>
+       <a href="{*[1]/@definitionURL}">
+       <FONT color="green" FACE="symbol">
+        <xsl:text>&#x00de;</xsl:text>
+       </FONT>
+       <SUB>
+        <FONT color="green" FACE="symbol">
+         <xsl:text>&#x0062;</xsl:text>
+        </FONT>
+       </SUB>
+       </a>
+       <xsl:apply-templates select="*[3]" mode="inline"/>
+      </xsl:when>
+
+      <xsl:when test="$name='par_beta_red'">
+       <xsl:apply-templates select="*[2]" mode="inline"/>
+       <a href="{*[1]/@definitionURL}">
+       <FONT color="green" FACE="symbol">
+        <xsl:text>&#x00de;</xsl:text>
+       </FONT>
+       <SUB>
+        <FONT color="green" FACE="symbol">
+         <xsl:text>&#x0062;*</xsl:text>
+        </FONT>
+       </SUB>
+       </a>
+       <xsl:apply-templates select="*[3]" mode="inline"/>
+      </xsl:when>
+
+      <!-- forgetful -->
+      <xsl:when test="$name='forgetful'">
+       <a href="{*[1]/@definitionURL}">|</a>
+       <xsl:apply-templates select="*[2]" mode="inline"/>
+       <a href="{*[1]/@definitionURL}">|</a>
+      </xsl:when>
+ 
+      <!-- boolean algebra of redexes -->
+
+      <!-- isomorphic -->
+      <xsl:when test="$name='isomorphic'">
+       <xsl:apply-templates select="*[2]" mode="inline"/>
+       <a href="{*[1]/@definitionURL}">
+        <FONT color="green" FACE="symbol">
+        <xsl:text>&#x0040;</xsl:text>
+       </FONT>
+       </a>
+       <xsl:apply-templates select="*[3]" mode="inline"/>
+      </xsl:when>
 
       <!-- INTERP -->
       <xsl:when test="$name='interp'">

diff --git a/helm/style/headercontent.xsl b/helm/style/headercontent.xsl
index 760010530a7b22c181319849b1b46900993dd015..a46023db59403204746ebd00dae04f4ab5e1a493 100644 (file)
--- a/helm/style/headercontent.xsl
+++ b/helm/style/headercontent.xsl
@@ -37,5 +37,6 @@
 <xsl:include href="set.xsl"/>
 <xsl:include href="reals.xsl"/>
 <xsl:include href="ring.xsl"/>        <!-- FG -->
+<xsl:include href="lambda.xsl"/>
 
 </xsl:stylesheet>