From: Irene Schena <irene.schena@unibo.it>
Date: Thu, 26 Jul 2001 15:49:26 +0000 (+0000)
Subject: ----------------------------------------------------------------------
X-Git-Tag: v0_1_3~98
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=09d83294deadf767b033b1dd37bc2f902918ccc9;p=helm.git

----------------------------------------------------------------------
Modified Files:
1) mmlextension.xsl: added notation for lambda calculus
----------------------------------------------------------------------
---

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 21225aa86..71a424d8b 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -1520,6 +1520,135 @@ which generates the toplevel element (see for instance xlink) -->
          </m:mtr>
         </m:mtable>
       </xsl:when>
+      <!-- ***************************************** -->
+      <!-- *********** NOTATIONS ******************* -->
+      <!-- ***************************************** -->
+      <!-- subst -->
+      <xsl:when test="$name='subst'">
+        <xsl:apply-templates select="*[3]"/>
+        <m:mo>&#xe8a0;</m:mo>
+        <m:mrow>
+         <m:mo stretchy="false">[</m:mo>
+         <m:mrow>
+          <xsl:apply-templates select="*[4]"/>
+          <m:mo mathcolor="green">
+           <xsl:if test="$id != ''">
+            <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+           </xsl:if>&#8592;</m:mo>
+          <xsl:apply-templates select="*[2]"/>
+         </m:mrow>
+         <m:mo stretchy="false">]</m:mo>
+        </m:mrow>
+      </xsl:when>
+      <!-- lift -->
+      <xsl:when test="$name='lift'">
+        <m:msup>
+         <m:mo mathcolor="green">
+          <xsl:if test="$id != ''">
+           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+          </xsl:if>&#8593;</m:mo>
+	 <xsl:apply-templates select="*[2]"/>
+        </m:msup>
+	<m:mrow>
+	 <m:mo stretchy="false">(</m:mo>
+         <xsl:apply-templates select="*[3]"/>
+	 <m:mo stretchy="false">)</m:mo>
+        </m:mrow>
+      </xsl:when>
+      <!-- lift_with_base -->
+      <xsl:when test="$name='lift_with_base'">
+        <m:msubsup>
+         <m:mo mathcolor="green">
+          <xsl:if test="$id != ''">
+           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+          </xsl:if>&#8593;</m:mo>
+	 <xsl:apply-templates select="*[3]"/>
+	 <xsl:apply-templates select="*[4]"/>
+        </m:msubsup>
+	<m:mrow>
+	 <m:mo stretchy="false">(</m:mo>
+         <xsl:apply-templates select="*[2]"/>
+	 <m:mo stretchy="false">)</m:mo>
+        </m:mrow>	
+      </xsl:when>
+      <!-- beta_red1 -->
+      <xsl:when test="$name='beta_red1'">
+        <xsl:apply-templates select="*[2]"/>
+        <m:munder>
+         <m:mo mathcolor="green">
+          <xsl:if test="$id != ''">
+           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+          </xsl:if>&#8594;</m:mo>
+          <m:mi mathcolor="green">&#946;</m:mi>
+        </m:munder>
+        <xsl:apply-templates select="*[3]"/>
+      </xsl:when>
+      <!-- beta_red -->
+      <xsl:when test="$name='beta_red'">
+        <xsl:apply-templates select="*[2]"/>
+        <m:munderover>
+         <m:mo mathcolor="green">
+          <xsl:if test="$id != ''">
+           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+          </xsl:if>&#8594;</m:mo>
+          <m:mi mathcolor="green">&#946;</m:mi>
+          <m:mi mathcolor="green">*</m:mi>
+        </m:munderover>
+        <xsl:apply-templates select="*[3]"/>
+      </xsl:when>
+      <!-- par_beta_red1 -->
+      <xsl:when test="$name='par_beta_red1'">
+        <xsl:apply-templates select="*[2]"/>
+        <m:munder>
+         <m:mo mathcolor="green">
+          <xsl:if test="$id != ''">
+           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+          </xsl:if>&#8658;</m:mo>
+          <m:mi mathcolor="green">&#946;</m:mi>
+        </m:munder>
+        <xsl:apply-templates select="*[3]"/>
+      </xsl:when>
+      <!-- par_beta_red -->
+      <xsl:when test="$name='par_beta_red'">
+        <xsl:apply-templates select="*[2]"/>
+        <m:munderover>
+         <m:mo mathcolor="green">
+          <xsl:if test="$id != ''">
+           <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+          </xsl:if>&#8658;</m:mo>
+          <m:mi mathcolor="green">&#946;</m:mi>
+          <m:mi mathcolor="green">*</m:mi>
+        </m:munderover>
+        <xsl:apply-templates select="*[3]"/>
+      </xsl:when>
+      <!-- forgetful -->
+      <xsl:when test="$name='forgetful'">
+       <m:mfenced open="|" close="|">
+        <xsl:if test="$id != ''">
+         <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+        </xsl:if>
+        <xsl:apply-templates select="*[2]"/>
+       </m:mfenced>
+      </xsl:when>
+      <!-- isomorphic -->
+      <xsl:when test="$name='isomorphic'">
+        <xsl:apply-templates select="*[2]"/>
+        <m:mo mathcolor="green">
+         <xsl:if test="$id != ''">
+          <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+         </xsl:if>&#8773;</m:mo>
+        <xsl:apply-templates select="*[3]"/>
+      </xsl:when>
+      <!-- interp -->
+      <xsl:when test="$name='forgetful'">
+       <m:mfenced open="[" close="]">
+        <xsl:if test="$id != ''">
+         <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+        </xsl:if>
+        <xsl:apply-templates select="*[2]"/>
+       </m:mfenced>
+      </xsl:when> 
+
       <!-- ERROR -->
       <xsl:otherwise>
        <m:mi>ERROR</m:mi>