Proof explosion improved (= avoided) for:

 1) Proofs after lambda-introductions (linear proofs)
 2) Proofs after a rewriting step (linear proofs)
 3) Proofs after a letin1 (linear proofs)

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 75c8a745be217d541858131a263a29824fa8f94d..d0c8555b39ac48df5c4a91c1469350ffcff0dfdb 100644 (file)
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -988,8 +988,12 @@ which generates the toplevel element (see for instance xlink) -->
       <!-- PROOF -->
       <xsl:when test="$name='proof'">
        <m:maction actiontype="toggle">
-        <!-- CSC: next if until the annotationHelper can handle mactions -->
-        <xsl:if test="not($explodeall)">
+        <!-- CSC: $explodeall until the annotationHelper can handle mactions -->
+        <xsl:variable name="test" select="(not($explodeall)) and
+          (not(preceding-sibling::*[1]/text()='letin1')) and
+          (not(preceding-sibling::*[1]/text()='rw_step')) and
+          (not(name(..)='m:lambda'))"/>
+        <xsl:if test="$test">
          <!-- Details hided (default) -->
          <m:mtable align="baseline 1" equalrows="false" columnalign="left">
           <m:mtr>
@@ -1026,7 +1030,9 @@ which generates the toplevel element (see for instance xlink) -->
              <m:mphantom>
               <m:mtext>_</m:mtext>
              </m:mphantom>
-             <m:mtext mathcolor="Green">(hide&#x00a0;details)</m:mtext>
+             <xsl:if test="$test">
+              <m:mtext mathcolor="Green">(hide&#x00a0;details)</m:mtext>
+             </xsl:if>
             </m:mrow>
            </m:mrow>
           </m:mtd>