]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/style/content.xsl
forall csymbol added
[helm.git] / helm / style / content.xsl
index 948cbbaecc1989cdadcdf89c915160c72063d84c..67c83efcf66a0e4d1dbe8cf8c5e39da77f2901c0 100644 (file)
@@ -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>