]> matita.cs.unibo.it Git - helm.git/commitdiff
----------------------------------------------------------------------
authorIrene Schena <irene.schena@unibo.it>
Thu, 26 Jul 2001 15:49:26 +0000 (15:49 +0000)
committerIrene Schena <irene.schena@unibo.it>
Thu, 26 Jul 2001 15:49:26 +0000 (15:49 +0000)
Modified Files:
1) mmlextension.xsl: added notation for lambda calculus
----------------------------------------------------------------------

helm/style/mmlextension.xsl

index 21225aa8638e98d0211d15eccc6a4d0ee7498f47..71a424d8bb52585e46c4b9aa829eee25a43e3021 100644 (file)
@@ -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>