]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/style/style_prima_del_linguaggio_naturale/content_to_html.xsl
Added style before natural language synthesis
[helm.git] / helm / style / style_prima_del_linguaggio_naturale / content_to_html.xsl
diff --git a/helm/style/style_prima_del_linguaggio_naturale/content_to_html.xsl b/helm/style/style_prima_del_linguaggio_naturale/content_to_html.xsl
new file mode 100644 (file)
index 0000000..dd1c077
--- /dev/null
@@ -0,0 +1,657 @@
+<?xml version="1.0"?>
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+                              xmlns:m="http://www.w3.org/1998/Math/MathML">
+
+<!--***********************************************************************--> 
+<!-- From MathML content to HTML                                           -->
+<!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                      -->
+<!--***********************************************************************--> 
+
+
+<xsl:include href="html_init.xsl"/>
+<xsl:include href="html_set.xsl"/>
+<xsl:include href="html_reals.xsl"/>
+
+
+<!-- <xsl:variable name="absPath">http://localhost:8081/get?url=</xsl:variable>-->
+<xsl:variable name="header" select="document('http://localhost:8081/conf')/html_link"/>
+
+<xsl:variable name="showcast" select="0"/>
+
+
+<!--***********************************************************************-->
+<!-- HTML Head and Body                                                    -->
+<!--***********************************************************************-->
+
+<xsl:output method="html"/>
+
+<xsl:variable name="framewidth" select="36"/>
+
+<xsl:template match="/">
+ <xsl:param name="current_indent" select="0"/>
+               <html> 
+                <head></head>
+                <body>
+                <xsl:apply-templates>
+                 <xsl:with-param name="current_indent" select="0"/>
+                </xsl:apply-templates>
+                </body>
+               </html>
+</xsl:template>
+
+<!--***********************************************************************-->
+<!-- Indentation                                                          -->
+<!--***********************************************************************-->
+
+<xsl:template name="make_indent">
+ <xsl:param name="current_indent" select="0"/>
+  <xsl:if test="$current_indent > 0">
+   <xsl:text>&#x00A0;</xsl:text>
+   <xsl:call-template name="make_indent">
+    <xsl:with-param name="current_indent" select="$current_indent - 1"/> 
+   </xsl:call-template>
+  </xsl:if>
+</xsl:template>
+
+<!-- Syntactic Sugar -->
+
+<xsl:template match="m:type">
+<xsl:param name="current_indent" select="0"/> 
+<xsl:apply-templates>
+ <xsl:with-param name="current_indent" 
+           select="$current_indent"/>
+</xsl:apply-templates>
+</xsl:template>
+
+<xsl:template match="m:condition">
+<xsl:param name="current_indent" select="0"/> 
+<xsl:apply-templates>
+ <xsl:with-param name="current_indent" 
+           select="$current_indent"/>
+</xsl:apply-templates>
+</xsl:template>
+
+<xsl:template match="m:math">
+<xsl:param name="current_indent" select="0"/> 
+<xsl:apply-templates>
+ <xsl:with-param name="current_indent" 
+           select="$current_indent"/>
+</xsl:apply-templates>
+</xsl:template>
+
+<!-- CSYMBOL -->
+
+<xsl:template match="m:apply[m:csymbol]">
+  <xsl:param name="current_indent" select="0"/> 
+  <xsl:param name="width" select="$framewidth"/> 
+  <xsl:variable name="name">
+   <xsl:value-of select="m:csymbol"/>
+  </xsl:variable>
+  <xsl:variable name="charlength">
+   <xsl:apply-templates select="m:csymbol" mode="charcount"/>
+  </xsl:variable>
+     <!-- <xsl:value-of select="$current_indent"/> -->
+     <!-- <xsl:value-of select="$charlength"/> -->
+     <xsl:choose>
+      <xsl:when test="$name='prod'">
+       <xsl:choose>
+       <xsl:when test="$charlength > $framewidth">
+         <!-- &#x03a0; -->
+         <FONT FACE="symbol" SIZE="+2" color="blue">&#80;</FONT>
+         <xsl:apply-templates select="m:bvar/m:ci"/>
+         <xsl:text>:</xsl:text>
+         <xsl:apply-templates select="m:bvar/m:type">
+          <xsl:with-param name="current_indent" 
+           select="$current_indent + 2 + string-length(m:bvar/m:ci)"/>
+         </xsl:apply-templates><BR/> 
+         <xsl:call-template name="make_indent">
+          <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
+         </xsl:call-template>
+         <xsl:text>.</xsl:text>
+         <xsl:apply-templates select="*[position()=3]">
+          <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+         </xsl:apply-templates>
+       </xsl:when>
+       <xsl:otherwise>
+        <!-- &#x03a0; -->
+        <FONT FACE="symbol" SIZE="+2" color="blue">&#80;</FONT>
+        <xsl:apply-templates select="m:bvar/m:ci"/>
+        <xsl:text>:</xsl:text>
+        <xsl:apply-templates select="m:bvar/m:type"/>
+        <xsl:text>.</xsl:text>
+        <xsl:apply-templates select="*[position()=3]"/>
+       </xsl:otherwise>
+       </xsl:choose>
+      </xsl:when>
+      <xsl:when test="$name='arrow'">
+       <xsl:choose>
+       <xsl:when test="$charlength > $framewidth">
+       <xsl:text>(</xsl:text>
+       <xsl:apply-templates select="*[position()=2]">
+        <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+       </xsl:apply-templates>
+       <BR/>
+       <xsl:call-template name="make_indent">
+        <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
+       </xsl:call-template>
+       <!-- -> -->
+       <FONT FACE="symbol" SIZE="+2" color="blue">&#174;</FONT>
+       <xsl:apply-templates select="*[position()=3]">
+        <xsl:with-param name="current_indent" select="$current_indent + 5"/>
+       </xsl:apply-templates>
+       <xsl:text>)</xsl:text>
+       </xsl:when>
+       <xsl:otherwise>
+        <xsl:text>(</xsl:text>
+        <xsl:apply-templates select="*[position()=2]"/>
+        <!-- -> -->
+        <FONT FACE="symbol" SIZE="+2" color="blue">&#174;</FONT>
+        <xsl:apply-templates select="*[position()=3]"/>
+        <xsl:text>)</xsl:text>
+       </xsl:otherwise>
+       </xsl:choose>
+      </xsl:when>
+      <xsl:when test="$name='app'">
+       <xsl:choose>
+       <xsl:when test="$charlength  > $framewidth">
+        <xsl:text>(</xsl:text>
+        <xsl:apply-templates select="*[position()=2]">
+         <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+        </xsl:apply-templates>
+         <xsl:for-each select="*[position()>2]">
+          <BR/>
+           <xsl:call-template name="make_indent">
+            <xsl:with-param name="current_indent" select="$current_indent + 2"/>         
+           </xsl:call-template>
+            <xsl:apply-templates select=".">
+             <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+            </xsl:apply-templates>
+         </xsl:for-each>
+         <xsl:text>)</xsl:text>
+       </xsl:when>
+       <xsl:otherwise>
+        <xsl:text>(</xsl:text>
+        <xsl:apply-templates select="*[position()=2]"/>
+        <xsl:for-each select="*[position()>2]">
+         <xsl:text>&#x00A0;</xsl:text>
+         <xsl:apply-templates select="."/>
+        </xsl:for-each>
+        <xsl:text>)</xsl:text>
+       </xsl:otherwise>
+       </xsl:choose>
+      </xsl:when>
+      <xsl:when test="$name='cast'">
+       <xsl:choose>
+        <xsl:when test="$showcast = 1">
+         <xsl:choose>
+          <xsl:when test="$charlength > $framewidth">
+           <xsl:text>(</xsl:text>
+           <xsl:apply-templates select="*[position()=2]">
+            <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+           </xsl:apply-templates><BR/>
+           <xsl:call-template name="make_indent">
+            <xsl:with-param name="current_indent" select="$current_indent + 2"/>          </xsl:call-template>
+           <xsl:text>:></xsl:text>
+           <xsl:apply-templates select="*[position()=3]">
+            <xsl:with-param name="current_indent" select="$current_indent + 3"/>
+           </xsl:apply-templates>
+           <xsl:text>)</xsl:text>
+          </xsl:when>
+          <xsl:otherwise>
+           <xsl:text>(</xsl:text>
+           <xsl:apply-templates select="*[position()=2]"/>
+           <xsl:text>:></xsl:text>
+           <xsl:apply-templates select="*[position()=3]"/>
+           <xsl:text>)</xsl:text>
+          </xsl:otherwise>
+         </xsl:choose>
+        </xsl:when>
+        <xsl:otherwise>
+         <xsl:apply-templates select="*[position()=2]">
+          <xsl:with-param name="current_indent" select="$current_indent"/>
+         </xsl:apply-templates>
+        </xsl:otherwise>
+       </xsl:choose>
+      </xsl:when>
+      <xsl:when test="$name='Prop'">
+       <xsl:text>Prop</xsl:text>
+      </xsl:when>
+      <xsl:when test="$name='Set'">
+       <xsl:text>Set</xsl:text>
+      </xsl:when>
+      <xsl:when test="$name='Type'">
+       <xsl:text>Type</xsl:text>
+      </xsl:when>
+      <xsl:when test="$name='mutcase'">
+       <xsl:choose>
+       <xsl:when test="$charlength > $framewidth">
+         <xsl:text>&lt;</xsl:text>
+         <xsl:apply-templates select="*[position()=2]">
+          <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+         </xsl:apply-templates>
+         <xsl:text>&gt; </xsl:text>
+         <xsl:text>CASE </xsl:text>
+         <xsl:apply-templates select="*[position()=3]">
+          <xsl:with-param name="current_indent" select="$current_indent + 8"/>
+         </xsl:apply-templates>
+         <xsl:text> OF </xsl:text> 
+         <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
+         <BR/>
+         <xsl:call-template name="make_indent">
+            <xsl:with-param name="current_indent" select="$current_indent + 2"/>  
+         </xsl:call-template> 
+            <xsl:choose>
+            <xsl:when test="position() = 1">
+             <xsl:text>&#x00A0;&#x00A0;</xsl:text>
+            </xsl:when>
+            <xsl:otherwise>
+             <xsl:text>| </xsl:text>
+            </xsl:otherwise>
+            </xsl:choose>
+            <xsl:apply-templates select="."/>
+            <FONT FACE="symbol" SIZE="+2" color="green">&#222;</FONT>
+            <xsl:apply-templates select="following-sibling::*[position()= 1]">
+             <xsl:with-param name="current_indent" select="$current_indent + 4 + string-length()"/>
+            </xsl:apply-templates>
+         </xsl:for-each>
+       </xsl:when>
+       <xsl:otherwise>
+        <xsl:text>&lt;</xsl:text> 
+        <xsl:apply-templates select="*[position()=2]"/> 
+        <xsl:text>&gt; </xsl:text>
+        <xsl:text>CASE </xsl:text>
+        <xsl:apply-templates select="*[position()=3]"/>
+        <xsl:text> OF </xsl:text>
+        <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
+         <xsl:choose>
+         <xsl:when test="not(position() = 1)">
+          <xsl:text> | </xsl:text> 
+         </xsl:when> 
+         </xsl:choose>
+         <xsl:apply-templates select="."/>
+         <FONT FACE="symbol" SIZE="+2" color="green">&#222;</FONT>
+         <xsl:apply-templates select="following-sibling::*[position()= 1]">
+          <xsl:with-param name="current_indent" select="$current_indent + 2 + string-length()"/>
+         </xsl:apply-templates>
+        </xsl:for-each>
+       </xsl:otherwise>
+       </xsl:choose>
+      </xsl:when>
+      <xsl:when test="$name='fix'">
+       <xsl:choose>
+       <xsl:when test="$charlength  > $framewidth">
+            <xsl:text>FIX</xsl:text>
+            <xsl:value-of select="m:ci"/>
+            <xsl:text>{</xsl:text> 
+            <xsl:for-each select="m:bvar"> 
+              <BR/>
+              <xsl:call-template name="make_indent">
+               <xsl:with-param name="current_indent" select="$current_indent + 2"/>  
+              </xsl:call-template>
+              <xsl:value-of select="m:ci"/>
+              <xsl:text>:</xsl:text>
+              <xsl:apply-templates select="m:type">
+               <xsl:with-param name="current_indent" 
+                    select="$current_indent + 5 + string-length(m:ci)"/>
+               </xsl:apply-templates>
+              <BR/>
+              <xsl:call-template name="make_indent">
+               <xsl:with-param name="current_indent" select="$current_indent + 2"/>       
+              </xsl:call-template>
+              <xsl:text>:=</xsl:text> 
+              <xsl:apply-templates select="following-sibling::*[position() = 1]">
+               <xsl:with-param name="current_indent" select="$current_indent +2"/>
+              </xsl:apply-templates>
+            </xsl:for-each>
+             <BR/>
+              <xsl:call-template name="make_indent">
+               <xsl:with-param name="current_indent" select="$current_indent + 2"/>       
+              </xsl:call-template> 
+           <xsl:text>}</xsl:text>
+       </xsl:when>
+       <xsl:otherwise>
+        <xsl:text>FIX</xsl:text>
+        <xsl:value-of select="m:ci"/>
+        <xsl:text>{</xsl:text>
+        <xsl:for-each select="m:bvar"> 
+            <xsl:value-of select="m:ci"/>
+            <xsl:text>:</xsl:text>
+            <xsl:apply-templates select="m:type"/>
+            <xsl:text>:=</xsl:text>
+            <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
+            <xsl:choose>
+             <xsl:when test="position()=last()">
+             <xsl:text>}</xsl:text>
+             </xsl:when>
+             <xsl:otherwise>
+             <xsl:text>;</xsl:text>
+             </xsl:otherwise>
+            </xsl:choose>
+         </xsl:for-each>
+       </xsl:otherwise>
+       </xsl:choose>
+      </xsl:when> 
+      <xsl:when test="$name='cofix'">
+       <xsl:choose>
+       <xsl:when test="($charlength + 10) > $framewidth">
+            <xsl:text>COFIX</xsl:text>
+            <xsl:value-of select="m:ci"/>
+            <xsl:text>{</xsl:text>
+            <BR/>
+            <xsl:call-template name="make_indent">
+             <xsl:with-param name="current_indent" select="$current_indent + 2"/>       
+            </xsl:call-template>
+            <xsl:for-each select="m:bvar"> 
+                <xsl:value-of select="m:ci"/>
+                <xsl:text>:</xsl:text>
+                <xsl:apply-templates select="m:type">
+                 <xsl:with-param name="current_indent" 
+                    select="$current_indent + 5 + string-length(m:ci)"/>
+                </xsl:apply-templates>
+                <BR/> 
+                <xsl:call-template name="make_indent">
+                 <xsl:with-param name="current_indent" select="$current_indent + 2"/>       
+                </xsl:call-template>
+                <xsl:text>:=</xsl:text>
+                <xsl:apply-templates select="following-sibling::*[position() = 1]">
+                 <xsl:with-param name="current_indent" select="$current_indent + 3"/>
+                </xsl:apply-templates>
+            </xsl:for-each>
+            <BR/>
+              <xsl:call-template name="make_indent">
+               <xsl:with-param name="current_indent" select="$current_indent + 2"/>       
+              </xsl:call-template>
+            <xsl:text>}</xsl:text>
+       </xsl:when>
+       <xsl:otherwise>
+        <xsl:text>COFIX</xsl:text>
+        <xsl:value-of select="m:ci"/>
+        <xsl:text>{</xsl:text>
+        <xsl:for-each select="m:bvar"> 
+            <xsl:value-of select="m:ci"/>
+            <xsl:text>:</xsl:text>
+            <xsl:apply-templates select="m:type"/>
+            <xsl:text>:=</xsl:text>
+            <xsl:apply-templates select="following-sibling::*[position() = 1]"/>
+            <xsl:choose>
+             <xsl:when test="position()=last()">
+             <xsl:text>}</xsl:text>
+             </xsl:when>
+             <xsl:otherwise>
+             <xsl:text>;</xsl:text>
+             </xsl:otherwise>
+            </xsl:choose>
+         </xsl:for-each>
+       </xsl:otherwise>
+       </xsl:choose>
+      </xsl:when>
+      </xsl:choose>
+    <!--  </m:mrow> -->
+</xsl:template>
+
+<!-- LAMBDA -->
+
+<xsl:template match="m:lambda">
+<xsl:param name="current_indent" select="0"/>
+    <xsl:variable name="charlength">
+     <xsl:apply-templates select="*[position()=1]" mode="charcount"/>
+     <!-- <xsl:apply-templates select="." mode="charcount"/> -->
+    </xsl:variable>
+    <!-- <xsl:value-of select="$charlength"/> -->
+     <xsl:choose>
+     <xsl:when test="$charlength > $framewidth">
+       <!-- &#x03bb; -->
+       <FONT FACE="symbol" SIZE="+2" color="red">&#108;</FONT>
+       <xsl:apply-templates select="m:bvar/m:ci"/>
+       <xsl:text>:</xsl:text>
+       <xsl:apply-templates select="m:bvar/m:type">
+        <xsl:with-param name="current_indent" 
+           select="$current_indent + 2 + string-length(m:bvar/m:ci)"/>
+       </xsl:apply-templates><BR/> 
+       <xsl:call-template name="make_indent">
+        <xsl:with-param name="current_indent" select="$current_indent + 2"/>       
+       </xsl:call-template>
+       <xsl:text>.</xsl:text>
+       <xsl:apply-templates select="*[position()=2]">
+        <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+       </xsl:apply-templates>
+     </xsl:when>
+     <xsl:otherwise>
+      <!-- &#x03bb; -->
+      <FONT FACE="symbol" SIZE="+2" color="red">&#108;</FONT>
+      <xsl:apply-templates select="m:bvar/m:ci"/>
+      <xsl:text>:</xsl:text>
+      <xsl:apply-templates select="m:bvar/m:type"/>
+      <xsl:text>.</xsl:text>
+      <xsl:apply-templates select="*[position()=2]"/>
+     </xsl:otherwise>
+     </xsl:choose>
+</xsl:template>
+
+<!-- href -->
+<xsl:template match="m:ci">
+ <xsl:choose>
+  <xsl:when test="boolean(@definitionURL)">
+<!-- CSC: non bisogna piu' utilizzare la url, bensi' la uri -->
+<!--   <xsl:variable name="url">
+    <xsl:value-of select="concat(string($absPath),
+     @definitionURL)"/>
+   </xsl:variable>-->
+   <a>
+   <xsl:attribute name="href">
+    <xsl:value-of select="concat(string($header),string(@definitionURL))"/>
+   </xsl:attribute>
+   <xsl:apply-templates/>
+   </a>
+  </xsl:when>
+  <xsl:otherwise>
+   <xsl:value-of select="."/>
+  </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+<!-- COUNTING -->
+
+<xsl:template match="m:ci|m:csymbol" mode="charcount">
+<xsl:param name="incurrent_length" select="0"/> 
+    <xsl:choose>
+    <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
+     <xsl:variable name="siblength"><xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$incurrent_length + string-length()"/></xsl:apply-templates></xsl:variable>
+     <xsl:choose>
+     <xsl:when test="string($siblength) = &quot;&quot;">
+      <xsl:value-of select="$incurrent_length + string-length()"/>
+     </xsl:when>
+     <xsl:otherwise>
+      <xsl:value-of select="number($siblength)"/>
+     </xsl:otherwise>
+     </xsl:choose>
+    </xsl:when>
+    <xsl:otherwise>
+     <xsl:value-of select="$incurrent_length + string-length()"/>
+    </xsl:otherwise>
+    </xsl:choose>
+</xsl:template> 
+
+<xsl:template match="*" mode="charcount">
+ <xsl:param name="incurrent_length" select="0"/>
+ <xsl:choose>
+  <xsl:when test="count(child::*) = 0">
+   <xsl:value-of select="$incurrent_length"/>
+  </xsl:when>
+  <xsl:otherwise>
+    <xsl:variable name="childlength"><xsl:apply-templates select="*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$incurrent_length"/></xsl:apply-templates></xsl:variable>
+    <xsl:choose>
+     <xsl:when test="$framewidth >= number($childlength)">
+      <xsl:variable name="siblength"><xsl:apply-templates select="following-sibling::*[position()=1]" mode="charcount"><xsl:with-param name="incurrent_length" select="$childlength"/></xsl:apply-templates></xsl:variable>
+      <xsl:choose>
+       <xsl:when test="string($siblength) = &quot;&quot;">
+        <xsl:value-of select="number($childlength)"/>
+       </xsl:when>
+       <xsl:otherwise>
+        <xsl:value-of select="number($siblength)"/>
+       </xsl:otherwise>
+      </xsl:choose>
+     </xsl:when>
+     <xsl:otherwise>
+      <xsl:value-of select="number($childlength)"/>
+     </xsl:otherwise>
+    </xsl:choose>
+  </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+
+<!--***********************************************************************-->
+<!-- OBJECTS                                                               -->
+<!--***********************************************************************-->
+
+<!-- DEFINITION -->
+
+<xsl:template match="Definition">
+<xsl:param name="current_indent" select="0"/>
+<p>
+DEFINITION <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<BR/>
+TYPE =<BR/>
+      <xsl:call-template name="make_indent">
+       <xsl:with-param name="current_indent" select="$current_indent + 7"/> 
+      </xsl:call-template>
+       <xsl:apply-templates select="type/*[1]">
+        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
+       </xsl:apply-templates><BR/>
+BODY =<BR/>
+      <xsl:call-template name="make_indent">
+       <xsl:with-param name="current_indent" select="$current_indent + 7"/> 
+      </xsl:call-template>
+       <xsl:apply-templates select="body/*[1]">
+        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
+       </xsl:apply-templates>
+</p>
+</xsl:template>
+
+<!-- AXIOM -->
+
+<xsl:template match="Axiom">
+<xsl:param name="current_indent" select="0"/>
+<p>
+AXIOM <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<BR/>
+TYPE = <xsl:apply-templates select="type/*[1]">
+          <xsl:with-param name="current_indent" select="$current_indent + 7"/>
+       </xsl:apply-templates>
+</p>
+</xsl:template>
+
+<!-- UNFINISHED PROOF -->
+
+<xsl:template match="CurrentProof">
+<xsl:param name="current_indent" select="0"/>
+<p>
+UNFINISHED PROOF <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != &quot;&quot;"><xsl:value-of select="Params"/></xsl:if>)<BR/>
+THESIS:  <xsl:apply-templates select="type/*[1]">
+          <xsl:with-param name="current_indent" select="$current_indent + 8"/>
+         </xsl:apply-templates><BR/>
+CONJECTURES: 
+      <xsl:for-each select="Conjecture">
+      <BR/>
+      <xsl:call-template name="make_indent">
+       <xsl:with-param name="current_indent" select="$current_indent + 8"/> 
+      </xsl:call-template>
+      <xsl:value-of select="./@no"/> : 
+      <xsl:apply-templates select="./*[1]">
+       <xsl:with-param name="current_indent" select="$current_indent + 11"/>
+      </xsl:apply-templates>
+      </xsl:for-each> 
+      <BR/>
+PROOF:
+      <xsl:apply-templates select="body/*[1]">
+        <xsl:with-param name="current_indent" select="$current_indent + 8"/>
+      </xsl:apply-templates>
+</p>
+</xsl:template>
+
+<!-- MUTUAL INDUCTIVE DEFINITION -->
+
+<xsl:template match="InductiveDefinition">
+<xsl:param name="current_indent" select="0"/>
+<p>
+     <xsl:for-each select="InductiveType">
+         <xsl:choose>
+         <xsl:when test="position() = 1">
+          <xsl:choose>
+          <xsl:when test="string(./@inductive) = &quot;true&quot;">
+          INDUCTIVE DEFINITION 
+          </xsl:when>
+          <xsl:otherwise>
+          COINDUCTIVE DEFINITION 
+          </xsl:otherwise>
+          </xsl:choose>  
+         </xsl:when>
+         <xsl:otherwise>
+          AND 
+         </xsl:otherwise>
+         </xsl:choose>
+         <xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != &quot;&quot;"><xsl:value-of select="../Params"/></xsl:if>)
+         [
+          <xsl:if test="string(../Param) != &quot;&quot;">         
+           <xsl:for-each select="../Param">
+            <xsl:value-of select="./@name"/>
+            :
+            <xsl:apply-templates select="*"/>
+           </xsl:for-each>
+          </xsl:if>
+         ] <BR/>
+         OF ARITY 
+         <xsl:apply-templates select="./arity/*[1]">
+          <xsl:with-param name="current_indent" select="$current_indent + 9"/>
+         </xsl:apply-templates> <BR/>
+         BUILT FROM:
+      <xsl:for-each select="./Constructor">
+      <BR/>
+      <xsl:call-template name="make_indent">
+       <xsl:with-param name="current_indent" select="$current_indent + 3"/> 
+      </xsl:call-template>
+         <xsl:choose>
+         <xsl:when test="position() = 1">
+         <xsl:text>&#x00A0;&#x00A0;</xsl:text>
+         </xsl:when>
+         <xsl:otherwise>
+         <xsl:text>| </xsl:text>
+         </xsl:otherwise>
+         </xsl:choose>
+         <xsl:value-of select="./@name"/> 
+         <xsl:text>: </xsl:text>
+         <xsl:apply-templates select="./*[1]">
+          <xsl:with-param name="current_indent" select="$current_indent + string-length(./@name) + 4"/>
+         </xsl:apply-templates>
+      </xsl:for-each>
+     </xsl:for-each>
+</p>
+</xsl:template>
+
+<!-- VARIABLE -->
+
+<xsl:template match="Variable">
+<xsl:param name="current_indent" select="0"/>
+<p>
+VARIABLE <xsl:value-of select="@name"/><BR/>
+TYPE = <xsl:apply-templates select="type/*[1]">
+          <xsl:with-param name="current_indent" select="$current_indent + 7"/>
+       </xsl:apply-templates>
+</p>
+</xsl:template>
+
+<!--***********************************************************************-->
+<!-- SECTIONS                                                              -->
+<!--***********************************************************************-->
+
+<!-- SECTION -->
+
+<xsl:template match="SECTION">
+<xsl:param name="current_indent" select="0"/>
+ <h1>BEGIN OF SECTION</h1>
+  <xsl:apply-templates/>
+ <h1>END OF SECTION</h1>
+</xsl:template>
+
+</xsl:stylesheet>