From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 7 Dec 2000 12:34:23 +0000 (+0000)
Subject: forall csymbol added
X-Git-Tag: nogzip~104
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=aa12f8cd84908fb3757a582cadd36ef49e269a2b;p=helm.git

forall csymbol added
---

diff --git a/helm/style/content.xsl b/helm/style/content.xsl
index 948cbbaec..67c83efcf 100644
--- a/helm/style/content.xsl
+++ b/helm/style/content.xsl
@@ -63,7 +63,14 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
       <xsl:apply-templates select="source/*[1]" mode="noannot"/>
      </xsl:when>
      <xsl:otherwise>
-      <m:csymbol>prod</m:csymbol>
+      <xsl:choose>
+       <xsl:when test="@type = 'Prop'">
+        <m:csymbol>forall</m:csymbol>
+       </xsl:when>
+       <xsl:otherwise>
+        <m:csymbol>prod</m:csymbol>
+       </xsl:otherwise>
+      </xsl:choose>
        <m:bvar>
         <m:ci>
          <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="target/@binder"/></xsl:with-param></xsl:call-template>
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 0a11b4991..698e8fce5 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -349,6 +349,36 @@
       <xsl:attribute name="helm:xref"><xsl:value-of select="@helm:xref"/></xsl:attribute>
      </xsl:if>
      <xsl:choose>
+      <xsl:when test="$name='forall'">
+       <xsl:choose>
+       <xsl:when test="$charlength >= $framewidth">
+        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+         <m:mtr>
+          <m:mtd>
+            <m:mo color="Blue"><m:mchar name="ForAll"/></m:mo>
+            <xsl:apply-templates select="m:bvar"/>
+          </m:mtd>
+         </m:mtr>
+         <m:mtr>
+          <m:mtd>
+           <m:mrow>
+            <m:mo>.</m:mo>
+            <xsl:apply-templates select="*[position()=3]"/>
+           </m:mrow>
+          </m:mtd>
+         </m:mtr>
+        </m:mtable>
+       </xsl:when>
+       <xsl:otherwise>
+        <m:mo color="Blue"><m:mchar name="ForAll"/></m:mo>
+        <xsl:apply-templates select="m:bvar/m:ci"/>
+        <m:mo>:</m:mo>
+        <xsl:apply-templates select="m:bvar/m:type"/>
+        <m:mo>.</m:mo>
+        <xsl:apply-templates select="*[position()=3]"/>
+       </xsl:otherwise>
+       </xsl:choose> 
+      </xsl:when>
       <xsl:when test="$name='prod'">
        <xsl:choose>
        <xsl:when test="$charlength >= $framewidth">