I don't know

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 566ccdf0a131f5523545592cb2bbd7439db736f7..87e31e8aede6e02d8e4e8e803a25bac13cf9ec55 100644 (file)
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -803,6 +803,7 @@
           <m:mtd>
            <m:mrow>
             <m:mtext color="#b03060">we proved </m:mtext>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="*[position()=3]"/>
            </m:mrow>
           </m:mtd>
@@ -913,6 +914,7 @@
             <m:mtext>(</m:mtext>
             <xsl:apply-templates select="*[3]"/>
             <m:mtext>)</m:mtext>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="*[4]"/>
             </m:mrow>
           </m:mtd>
@@ -923,6 +925,7 @@
             <m:mtext>(</m:mtext>
             <xsl:apply-templates select="*[5]"/>
             <m:mtext>)</m:mtext>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="*[6]"/>
             </m:mrow>
           </m:mtd>
@@ -1012,6 +1015,8 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
+            <m:mtext color="#b03060">we get</m:mtext>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="."/>
            </m:mrow>
           </m:mtd>
@@ -1028,6 +1033,8 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
+            <m:mtext color="#b03060">we get</m:mtext>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="."/>
            </m:mrow>
           </m:mtd>

diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 8265e079e261615fe0dc374c51001dbd551160e7..a3f2a15078cdeed3588e53b6485dce568f5c28ac 100644 (file)
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -145,6 +145,7 @@
         <m:csymbol>thread</m:csymbol>
         <xsl:apply-templates mode="pure" select="//ALLTYPES/TYPE[@id=$id]"/>
         <m:apply>
+         <m:csymbol>app</m:csymbol>
          <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
         </m:apply>
         <xsl:apply-templates mode="thread" select="*[@id = //ALLTYPES/TYPE/@id]"/>