From a0da07547d92d5bcb9f9eac2399ccb6b700b9d03 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 29 Aug 2001 15:16:25 +0000
Subject: [PATCH] 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)

---
 helm/style/mmlextension.xsl | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 75c8a745b..d0c8555b3 100644
--- 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>
-- 
2.39.2