X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fnuprl_stylesheets%2Fnuprl_content_to_html2.xsl;fp=helm%2Fnuprl_stylesheets%2Fnuprl_content_to_html2.xsl;h=0000000000000000000000000000000000000000;hp=ef15f1961ab592f13a804062a9e9a558cba2f7ea;hb=1696761e4b8576e8ed81caa905fd108717019226;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1

diff --git a/helm/nuprl_stylesheets/nuprl_content_to_html2.xsl b/helm/nuprl_stylesheets/nuprl_content_to_html2.xsl
deleted file mode 100644
index ef15f1961..000000000
--- a/helm/nuprl_stylesheets/nuprl_content_to_html2.xsl
+++ /dev/null
@@ -1,3047 +0,0 @@
-<?xml version="1.0"?>
-
-<!-- Copyright (C) 2000, HELM Team                                     -->
-<!--                                                                   -->
-<!-- This file is part of HELM, an Hypertextual, Electronic            -->
-<!-- Library of Mathematics, developed at the Computer Science         -->
-<!-- Department, University of Bologna, Italy.                         -->
-<!--                                                                   -->
-<!-- HELM is free software; you can redistribute it and/or             -->
-<!-- modify it under the terms of the GNU General Public License       -->
-<!-- as published by the Free Software Foundation; either version 2    -->
-<!-- of the License, or (at your option) any later version.            -->
-<!--                                                                   -->
-<!-- HELM is distributed in the hope that it will be useful,           -->
-<!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
-<!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
-<!-- GNU General Public License for more details.                      -->
-<!--                                                                   -->
-<!-- You should have received a copy of the GNU General Public License -->
-<!-- along with HELM; if not, write to the Free Software               -->
-<!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
-<!-- MA  02111-1307, USA.                                              -->
-<!--                                                                   -->
-<!-- For details, see the HELM World-Wide-Web page,                    -->
-<!-- http://cs.unibo.it/helm/.                                         -->
-
-<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, Guidi               -->
-<!--***********************************************************************--> 
-
-<xsl:param name="CICURI" select="''"/>
-<xsl:param name="type" select="'standalone'"/>
-<xsl:param name="UNICODEvsSYMBOL" select="'symbol'"/>
-<xsl:param name="explode_tactics" select="false()"/>
-
-<xsl:include href="nuprl_html_arith.xsl"/>
-<xsl:include href="nuprl_html_basic.xsl"/>
-
-<xsl:variable name="showcast" select="0"/>
-
-<!--***********************************************************************-->
-<!-- HTML Head and Body                                                    -->
-<!--***********************************************************************-->
-
-<!-- <xsl:output method="html" encoding="iso-8859-1"/> -->
-
-<!-- document needs method="xml" and searches locally for the dtd if        -->
-<!-- doctype-system is specified (the dtd must exist locally for parsing).  -->
-<!-- For having output html must be media-type="html" and for having the    -->
-<!-- correct <br /> you must specify at least the remote dtd by means of    -->
-<!-- doctype-public                                                         -->
-
-<!-- Commentd out by Zack, a try-fix for NuPRL stylesheets with OCaml UWOBO -->
-<!--
-<xsl:output 
-	method="xml" 
-	encoding="iso-8859-1" 
-	media-type="text/html"
-	doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN" />
--->
-<xsl:output 
-	method="html" 
-	encoding="iso-8859-1" 
-	media-type="text/html"
-	doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN" />
-
-<xsl:variable name="framewidth" select="55"/>
-
-<!--forall-->
-  <xsl:variable name="forall">
-    <xsl:choose>
-      <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&quot;</xsl:when>
-      <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#x2200;</xsl:when>
-      <xsl:otherwise>???</xsl:otherwise>
-    </xsl:choose>
-  </xsl:variable>
-<!--lambda-->
-  <xsl:variable name="lambda">
-    <xsl:choose>
-      <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">l</xsl:when>
-      <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#x3BB;</xsl:when>
-      <xsl:otherwise>???</xsl:otherwise>
-    </xsl:choose>
-  </xsl:variable>
-<!--prod-->
-  <xsl:variable name="prod">
-    <xsl:choose>
-      <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&#xD5;</xsl:when>
-      <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#x3A0;</xsl:when>
-      <xsl:otherwise>???</xsl:otherwise>
-    </xsl:choose>
-  </xsl:variable>
-<!--arrow-->
-  <xsl:variable name="arrow">
-    <xsl:choose>
-      <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&#xAE;</xsl:when>
-      <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#x2192;</xsl:when>
-      <xsl:otherwise>???</xsl:otherwise>
-    </xsl:choose>
-  </xsl:variable>
-<!--RightArrow-->
-  <xsl:variable name="RightArrow">
-    <xsl:choose>
-      <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&#xDE;</xsl:when>
-      <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#x21D2;</xsl:when>
-      <xsl:otherwise>???</xsl:otherwise>
-    </xsl:choose>
-  </xsl:variable>
-<!--product-->
-  <xsl:variable name="product">
-    <xsl:choose>
-      <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">S</xsl:when>
-      <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#931;</xsl:when>
-      <xsl:otherwise>???</xsl:otherwise>
-    </xsl:choose>
-  </xsl:variable>
-<!--member-->
-  <xsl:variable name="member">
-    <xsl:choose>
-      <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&#xce;</xsl:when>
-      <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#8712;</xsl:when>
-      <xsl:otherwise>???</xsl:otherwise>
-    </xsl:choose>
-  </xsl:variable>
-<!--member-->
-  <xsl:variable name="intersection">
-    <xsl:choose>
-      <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&#xc7;</xsl:when>
-      <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#8745;</xsl:when>
-      <xsl:otherwise>???</xsl:otherwise>
-    </xsl:choose>
-  </xsl:variable>
-<!--integers-->
-  <xsl:variable name="integers">
-    <xsl:choose>
-      <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">I</xsl:when>
-      <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#921;</xsl:when>
-      <xsl:otherwise>???</xsl:otherwise>
-    </xsl:choose>
-  </xsl:variable>
-<!--naturalnumbers-->
-  <xsl:variable name="naturalnumbers">
-    <xsl:choose>
-      <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">N</xsl:when>
-      <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#925;</xsl:when>
-      <xsl:otherwise>???</xsl:otherwise>
-    </xsl:choose>
-  </xsl:variable>
-<!--implies-->
-  <xsl:variable name="implies">
-    <xsl:choose>
-      <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&#xee;</xsl:when>
-      <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#8658;</xsl:when>
-      <xsl:otherwise>???</xsl:otherwise>
-    </xsl:choose>
-  </xsl:variable>
-<!--exists-->
-  <xsl:variable name="NUPRLexists">
-    <xsl:choose>
-      <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">&#x24;</xsl:when>
-      <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">&#8707;</xsl:when>
-      <xsl:otherwise>???</xsl:otherwise>
-    </xsl:choose>
-  </xsl:variable>
-
-
-
-<xsl:template name="mksymbol">
-        <xsl:param name="symbol" select="'???'"/>
-        <xsl:param name="color"  select="'blue'"/>
-        <xsl:param name="size"   select="''"/>
-
-        <xsl:choose>
-                <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">
-                        <FONT FACE="symbol" SIZE="{$size}" COLOR="{$color}">
-                                <xsl:value-of select="$symbol"/>
-                        </FONT>
-                </xsl:when>
-                <xsl:otherwise>
-                        <FONT COLOR="{$color}">
-                                <xsl:value-of select="$symbol"/>
-                        </FONT>
-                </xsl:otherwise>
-        </xsl:choose>
-</xsl:template>
-
-<xsl:template match="/">
- <xsl:param name="current_indent" select="0"/>
- <xsl:choose>
-  <xsl:when test="$type = 'standalone'">
-   <html> 
-      <head>
-	 <title> <xsl:value-of select="$CICURI"/> </title> <!-- FG -->
-         <style> A { text-decoration: none } </style>
-         <script>
-          <xsl:text disable-output-escaping="yes">
-           <![CDATA[
-            function Hide(which){
-             if (!document.getElementById)
-              return
-             which.style.display="none"
-            }
-
-            function Show(which){
-             if (!document.getElementById)
-              return
-             which.style.display=""
-            }
-
-            document.to_be_deleted = new Array();
-          ]]>
-          </xsl:text>
-         </script>
-	</head>
-      <body bgcolor="white">
-         <xsl:attribute name="onLoad">
-          if(document.getElementById)
-           for(var i=0;i&lt;document.to_be_deleted.length;i++)
-            Hide(document.getElementById(document.to_be_deleted[i]));
-         </xsl:attribute>
-         <xsl:apply-templates>
-            <xsl:with-param name="current_indent" select="0"/>
-         </xsl:apply-templates>
-      </body>
-   </html>
-  </xsl:when>
-  <xsl:otherwise>
-   <to_be_embedded>
-    <xsl:apply-templates>
-     <xsl:with-param name="current_indent" select="0"/>
-    </xsl:apply-templates>
-   </to_be_embedded>
-  </xsl:otherwise>
- </xsl:choose>
-</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>
-
-
-
-<!--*********************************************************************-->
-<!--                         INLINE MODE                                 -->
-<!--*********************************************************************-->
-
-<!-- href -->
-<xsl:template mode="inline" match="m:ci">
- <xsl:choose>
-  <xsl:when test="boolean(@definitionURL)">
-   <a href="{@definitionURL}">
-   <xsl:apply-templates/>
-   </a>
-  </xsl:when>
-  <xsl:otherwise>
-   <xsl:value-of select="."/>
-  </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
-
-<!-- CSYMBOL -->
-
-<xsl:template match="m:apply[m:csymbol]" mode="inline">
- <xsl:param name="current_indent" select="0"/>
-   <xsl:variable name="name">
-    <xsl:value-of select="m:csymbol"/>
-   </xsl:variable>
-   <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
-   <xsl:choose>
-
-    <!-- FUNCTION-DIP (PROD) -->
-	<xsl:when test="$name='prod'">
-		<xsl:call-template name="mksymbol">
-			<xsl:with-param name="symbol" select="$prod"/>
-			<xsl:with-param name="color" select="'blue'"/>
-			<xsl:with-param name="size" select="'+2'"/>
-		</xsl:call-template>
-	 	<xsl:apply-templates select="m:bvar/m:ci"/>
-		<xsl:if test="m:bvar/m:ci=&quot;&quot;">
-			<xsl:text>""</xsl:text>
-	 	</xsl:if>
-         	<xsl:text>:</xsl:text>
-		<!--<xsl:if test="m:bvar/m:type/*[*]">
-			<xsl:text>( </xsl:text>
-		</xsl:if>-->
-         	<xsl:apply-templates select="m:bvar/m:type"/>
-		<!--<xsl:if test="m:bvar/m:type/*[*]">
-			<xsl:text>) </xsl:text>
-		</xsl:if>-->
-		<xsl:text>.</xsl:text>
-		<xsl:apply-templates select="*[position()=3]"/>
-	</xsl:when>
-	
-	<!-- ARROW --> <!-- FUNCTION (IND) -->
-    <xsl:when test="$name='arrow'">
-    	<xsl:text>(</xsl:text>
-     	<xsl:apply-templates mode="inline" select="*[position()=2]"/>
-     	<xsl:call-template name="mksymbol">
-      		<xsl:with-param name="symbol" select="$arrow"/>
-      		<xsl:with-param name="color" select="'blue'"/>
-      		<xsl:with-param name="size" select="'+0'"/>
-     	</xsl:call-template>
-     	<xsl:apply-templates  select="*[position()=3]"/>
-     	<xsl:text>)</xsl:text>
-    </xsl:when>
-
-    
-    <!-- FORALL -->
-    <xsl:when test="$name='forall'">
-     	<xsl:call-template name="mksymbol">
-      		<xsl:with-param name="symbol" select="$forall"/>
-      		<xsl:with-param name="color" select="'blue'"/>
-      		<xsl:with-param name="size" select="'+2'"/>
-     	</xsl:call-template>
-     	<xsl:apply-templates select="m:bvar/m:ci"/>
-     	<xsl:text>:</xsl:text>
-     	<!--<xsl:if test="count(m:bvar/m:type/m:apply/*) > 1">
-     		<xsl:text>(</xsl:text>
-     	</xsl:if>-->
-     	<xsl:apply-templates select="m:bvar/m:type"/>
-     	<!--<xsl:if test="count(m:bvar/m:type/m:apply/*) > 1">
-     		<xsl:text>)</xsl:text>
-     	</xsl:if>-->
-     	<xsl:text>.</xsl:text>
-     	<xsl:apply-templates select="*[position()=3]"/>
-   </xsl:when>
-   
-   
-    <!-- PRODUCT -->
-    <xsl:when test="$name='product'">
-    	<xsl:call-template name="mksymbol">
-		<xsl:with-param name="symbol" select="$product"/>
-		<xsl:with-param name="color" select="'blue'"/>
-		<xsl:with-param name="size" select="'+2'"/>
-	</xsl:call-template>
-     	<xsl:apply-templates select="m:bvar/m:ci"/>
-     	<xsl:text>:</xsl:text>
-     	<xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
-	<xsl:text>.</xsl:text>
-	<xsl:apply-templates select="*[position()=3]"/>
-    </xsl:when>
-    
-    <!-- PROD_IND -->
-    <xsl:when test="$name='product_ind'">
-     <FONT color="blue">
-     <xsl:text>( </xsl:text>
-     </FONT>
-     <xsl:apply-templates mode="inline" select="m:type"/>
-     <FONT color="blue" size="+2">
-     <xsl:text>x</xsl:text>
-     </FONT>
-     <xsl:apply-templates mode="inline" select="*[position()=3]"/>
-     <FONT color="blue">
-     <xsl:text> )</xsl:text>
-     </FONT>
-
-    </xsl:when>
-   
-   <!-- PAIR -->
-   <xsl:when test="$name='pair'">
-   	<FONT color="blue" size="+1">
-   	<xsl:text>&lt;</xsl:text>
-	</FONT>
-	<xsl:apply-templates select="*[2]"/>
-	<xsl:text>, </xsl:text>
-	<xsl:apply-templates select="*[3]"/>
-	<FONT color="blue" size="+1">
-   	<xsl:text>&gt;</xsl:text>
-	</FONT>
-   </xsl:when>
-
-   <!-- UNION -->
-   <xsl:when test="$name='union'">
-   	<xsl:apply-templates select="*[2]"/>
-	<FONT color="blue" size="+2">
-   	<xsl:text>+</xsl:text>
-	</FONT>
-	<xsl:apply-templates select="*[3]"/>
-  </xsl:when>
-
-  <!-- INL -->
-  <xsl:when test="$name='inl'">
-  	<FONT color="blue">
-   	<xsl:text>inl (</xsl:text>
-	</FONT>
-  	<xsl:apply-templates select="*[2]"/>
-	<FONT color="blue">
-   	<xsl:text> )</xsl:text>
-	</FONT>
-  </xsl:when>
-
-   <!-- INR -->
-  <xsl:when test="$name='inr'">
-  	<FONT color="blue" size="+1">
-   	<xsl:text>inr (</xsl:text>
-	</FONT>
-  	<xsl:apply-templates select="*[2]"/>
-	<FONT color="blue" size="+1">
-   	<xsl:text> )</xsl:text>
-	</FONT>
-  </xsl:when>
-
-	<!-- EQUAL -->
-	<xsl:when test="$name='equal'">
-		<xsl:apply-templates select="*[position()=3]"/>
-		<FONT color="blue" size="+1">
-		<xsl:text> = </xsl:text>
-		</FONT>
-       		<xsl:apply-templates select="*[position()=4]"/>
-		<xsl:text> </xsl:text>
-       		<xsl:call-template name="mksymbol">
-        	<xsl:with-param name="symbol" select="$member"/>
-        	<xsl:with-param name="color" select="'blue'"/>
-        	<xsl:with-param name="size" select="'+0'"/>
-       		</xsl:call-template>
-		<xsl:text> </xsl:text>
-       		<xsl:apply-templates select="*[position()=2]">
-        	 <xsl:with-param name="current_indent" select="$current_indent"/>
-       		</xsl:apply-templates>
-       	</xsl:when>
-       
-       <!-- CONS -->
-	<xsl:when test="$name='cons'">
-		<xsl:apply-templates select="*[2]"/>
-		<FONT color="blue">
-		<xsl:text>::</xsl:text>
-		</FONT>
-		<xsl:apply-templates select="*[3]"/>
-	</xsl:when>
-
-	<!-- REC -->
-
-	<xsl:when test="$name='rec'">
-		<FONT color="blue">
-		<xsl:text>rectype</xsl:text>
-		</FONT>
-		<xsl:apply-templates select="*[2]"/>
-		<FONT color="blue">
-		<xsl:text>=</xsl:text>
-		</FONT>
-		<xsl:apply-templates select="*[3]"/>
-	</xsl:when>
-
-
-	<!-- SET -->
-
-	<xsl:when test="$name='t_set'">
-		<FONT color="blue">
-		<xsl:text>{</xsl:text>
-		</FONT>
-		<xsl:choose>
-		<xsl:when test="m:bvar/m:ci">
-			<xsl:apply-templates select="m:bvar/m:ci"/>
-			<FONT color="blue">
-			<xsl:text>:</xsl:text>
-			</FONT>
-			<xsl:apply-templates select="m:bvar/m:type"/>
-		</xsl:when>
-		<xsl:otherwise>
-		<xsl:apply-templates select="m:bvar/m:type"/>
-		</xsl:otherwise>
-		</xsl:choose>
-		<FONT color="blue">
-		<xsl:text>|</xsl:text>
-		</FONT>
-		<xsl:apply-templates select="*[3]"/>
-		<FONT color="blue">
-			<xsl:text>}</xsl:text>
-		</FONT>
-
-	</xsl:when>
-
-  	<!-- ISECT -->
-
-	<xsl:when test="$name='isect'">
-		<xsl:call-template name="mksymbol">
-        	<xsl:with-param name="symbol" select="$intersection"/>
-        	<xsl:with-param name="color" select="'blue'"/>
-        	<xsl:with-param name="size" select="'+0'"/>
-       		</xsl:call-template>
-		<xsl:apply-templates select="m:bvar/m:ci"/>
-		<FONT color="blue">
-		<xsl:text>:</xsl:text>
-		</FONT>
-		<xsl:apply-templates select="m:bvar/m:type"/>
-		<FONT color="blue">
-		<xsl:text>.</xsl:text>
-		</FONT>
-		<xsl:apply-templates select="*[3]"/>
-	</xsl:when>
-
-	<!-- QUOTIENT --> 
-
-	<xsl:when test="$name='quotient'">
-		<xsl:apply-templates select="m:bvar[1]"/>
-		<xsl:text>,</xsl:text>
-		<xsl:apply-templates select="m:bvar[2]"/>
-		<FONT color="blue">
-		<xsl:text>:</xsl:text>
-		</FONT>
-		<xsl:apply-templates select="*[2]"/>
-		<FONT color="blue">
-		<xsl:text>//</xsl:text>
-		</FONT>
-		<xsl:apply-templates select="*[5]"/>
-	</xsl:when>
-
-	<!-- SO_LAMBDA -->
-	<xsl:when test="$name='so_lambda'">
-       			<xsl:call-template name="mksymbol">
-        			<xsl:with-param name="symbol" select="$lambda"/>
-        			<xsl:with-param name="color" select="'red'"/>
-        			<xsl:with-param name="size" select="'+2'"/>
-       			</xsl:call-template>
-       			<xsl:apply-templates select="m:apply[1]/*[2]"/>
-       			<xsl:text>.</xsl:text>
-       			<xsl:apply-templates select="*[3]"/>
-     </xsl:when>
-
-
-	<!-- SO_APPLY -->
-
-	<xsl:when test="$name='so_apply'">
-        	<xsl:text>(</xsl:text>
-        	<xsl:apply-templates select="*[position()=2]"/>
-       	  	<xsl:for-each select="*[position()>2]">
-      			<xsl:text>&#x00A0;</xsl:text>
-            		<xsl:apply-templates mode="inline" select="."/>
-         	</xsl:for-each>
-         	<xsl:text>)</xsl:text>
-      </xsl:when>
-   <!-- APP -->
-    <xsl:when test="$name='app'">
-     <!-- NuPRL rendering -->
-     <xsl:apply-templates mode="inline" select="*[position()=2]"/>
-     <xsl:if test="count(*) &gt; 2">
-      <xsl:text>(</xsl:text>
-      <xsl:for-each select="*[position() &gt; 2]">
-       <xsl:apply-templates select="." mode="inline"/>
-       <xsl:if test="not(position() = last())">
-        <xsl:text>,</xsl:text>
-       </xsl:if>
-      </xsl:for-each>
-      <xsl:text>)</xsl:text>
-     </xsl:if>
-     <!-- CIC rendering
-     <xsl:text>(</xsl:text>
-     <xsl:apply-templates mode="inline" select="*[position()=2]"/>
-     <xsl:for-each select="*[position()>2]">
-      <xsl:text>&#x00A0;</xsl:text>
-      <xsl:apply-templates mode="inline" select="."/>
-     </xsl:for-each>
-     <xsl:text>)</xsl:text>
-     -->
-    </xsl:when>
-    <!-- CAST -->
-    <xsl:when test="$name='cast'">
-     <xsl:text>(</xsl:text>
-     <xsl:apply-templates mode="inline" select="*[position()=2]"/>
-     <xsl:text>:></xsl:text>
-     <xsl:apply-templates mode="inline" select="*[position()=3]"/>
-     <xsl:text>)</xsl:text>
-    </xsl:when>
-    <xsl:when test="$name='Prop'">
-     <FONT color="violet">Prop</FONT>
-    </xsl:when>
-    <xsl:when test="$name='Set'">
-     <FONT color="violet">Set</FONT>
-    </xsl:when>
-    <xsl:when test="$name='Type'">
-     <FONT color="violet">Type</FONT>
-    </xsl:when>
-   
-   <!-- MUTCASE -->
-    <xsl:when test="$name='mutcase'">
-     <xsl:text>&lt;</xsl:text> 
-     <xsl:apply-templates mode="inline" select="*[position()=2]"/> 
-     <xsl:text>&gt; </xsl:text>
-     <FONT color="red">CASE </FONT>
-     <xsl:apply-templates mode="inline" select="*[position()=3]"/>
-     <FONT color="red"> OF </FONT>
-<xsl:for-each select="m:piecewise/m:piece">
-<!--<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 mode="inline" select="./*[2]"/>
-      <xsl:call-template name="mksymbol">
-       <xsl:with-param name="symbol" select="$RightArrow"/>
-       <xsl:with-param name="color" select="'green'"/>
-       <xsl:with-param name="size" select="'+0'"/>
-      </xsl:call-template>
-      <xsl:apply-templates mode="inline"
-           select="./*[1]"/>
-     </xsl:for-each>
-    </xsl:when>
-   
-   <!-- FIX -->
-    <xsl:when test="$name='fix'">
-     <FONT color="red">FIX</FONT>
-     <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 mode="inline" select="m:type"/>
-      <xsl:text>:=</xsl:text>
-      <xsl:apply-templates mode="inline" 
-             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:when>
-   
-   <!-- COFIX -->
-    <xsl:when test="$name='cofix'">
-     <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 mode="inline" select="m:type"/>
-      <xsl:text>:=</xsl:text>
-      <xsl:apply-templates mode="inline" 
-          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:when>
-   
-   <!-- proof -->
-    <xsl:when test="$name='proof' or $name='side_proof'">
-       <xsl:apply-templates mode="inline" select="*[position()=2]"/>
-       <FONT color="red">&#x00a0;proves&#x00a0;</FONT>
-       <xsl:apply-templates mode="inline" select="*[position()=3]"/>
-    </xsl:when>
-    <xsl:when test="$name='letin1'">
-     <xsl:text>letin1 (inline error)</xsl:text>
-    </xsl:when>
-    <!-- false_ind -->
-    <xsl:when test="$name='false_ind'">
-    <xsl:apply-templates mode="inline" select="*[3]"/>
-    <FONT color="red">Contradiction.</FONT>
-    </xsl:when>
-    <!-- and_ind -->
-    <xsl:when test="$name='and_ind'">
-     <FONT color="red">From&#x00a0;</FONT>
-     <xsl:apply-templates select="*[2]"/>
-     <FONT color="red">&#x00a0;we get</FONT>
-     (
-     <xsl:apply-templates select="*[3]"/>
-     )&#x00a0;
-     <xsl:apply-templates mode="inline" select="*[4]"/>
-     <FONT color="red">&#x00a0;and&#x00a0;</FONT>
-     (
-     <xsl:apply-templates select="*[5]"/>
-     )&#x00a0;
-     <xsl:apply-templates mode="inline" select="*[6]"/>
-     ;
-     <FONT color="red">&#x00a0;hence&#x00a0;</FONT>
-     <xsl:apply-templates mode="inline" select="*[7]"/>
-    </xsl:when>
-   </xsl:choose>
-</xsl:template>
-
-<xsl:template mode="inline" match="m:lambda">
-	<xsl:call-template name="mksymbol">
-       		<xsl:with-param name="symbol" select="$lambda"/>
-       		<xsl:with-param name="color" select="'red'"/>
-       		<xsl:with-param name="size" select="'+2'"/>
-      	</xsl:call-template>
-      
-      <!-- IN NuPrl non e' specificato il tipo -->
-      	<xsl:apply-templates select="m:bvar/m:ci"/>
-	<xsl:if test="m:bvar[m:mtype]">
-      		<xsl:text>:</xsl:text>
-      		<xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
-	</xsl:if>
-      	<xsl:text>.</xsl:text>
-      <xsl:apply-templates mode="inline" select="*[position()=2]"/>
-</xsl:template>
-
-<!--*********************************************************************-->
-<!--                       NORMAL MODE                                   -->
-<!--*********************************************************************-->
-
-<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:variable name="uri">
-     <xsl:value-of select="*[1]/@definitionURL"/>
-    </xsl:variable>
-     
-     
-     <xsl:choose>
-     
-     <!-- FUNCTION-DIP (PROD) -->
-     <xsl:when test="$name='prod'">
-       <xsl:choose>
-      		<xsl:when test="$charlength > $framewidth">
-			<xsl:call-template name="mksymbol">
-				<xsl:with-param name="symbol" select="$prod"/>
-				<xsl:with-param name="color" select="'blue'"/>
-				<xsl:with-param name="size" select="'+2'"/>
-			</xsl:call-template>
-	 		<xsl:apply-templates select="m:bvar/m:ci">
-			<xsl:with-param name="current_indent" select="$current_indent"/>
-         		</xsl:apply-templates>
-			<xsl:if test="m:bvar/m:ci=&quot;&quot;">
-				<xsl:text>""</xsl:text>
-	 		</xsl:if>
-         		<xsl:text>:</xsl:text>
-			<!--<xsl:if test="m:bvar/m:type/*[*]">
-				<xsl:text>( </xsl:text>
-			</xsl:if>-->
-         		<xsl:apply-templates select="m:bvar/m:type">
-          			<xsl:with-param name="current_indent" 
-           			select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
-         		</xsl:apply-templates>
-			<!--<xsl:if test="m:bvar/m:type/*[*]">
-				<xsl:text>) </xsl:text>
-			</xsl:if>-->
-         		<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>
-        		<xsl:apply-templates mode="inline" select="."/>
-       		</xsl:otherwise>
-       </xsl:choose>
-      </xsl:when>
-    
-    <!-- ARROW --> <!-- FUNCTION IND -->
-	<xsl:when test="$name='arrow'">
-       		<xsl:choose>
-       			<xsl:when test="$charlength > $framewidth">
-			<xsl:text>arrow</xsl:text>
-       			<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:call-template name="mksymbol">
-        			<xsl:with-param name="symbol" select="$arrow"/>
-        			<xsl:with-param name="color" select="'blue'"/>
-        			<xsl:with-param name="size" select="'+0'"/>
-       			</xsl:call-template>
-       			<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:apply-templates mode="inline" select="."/>
-       		</xsl:otherwise>
-	</xsl:choose>
-</xsl:when>
-
-     <!-- TYPE_OF --> 
-     <xsl:when test="$name='type_of'">
-       	<xsl:value-of select="*[2]"/>
-         <xsl:text>:</xsl:text>
-	<xsl:if test="count(*[3]/*) > 1">
-		<xsl:text>(</xsl:text>
-	</xsl:if>
-	<xsl:apply-templates select="*[3]"/>
-	<xsl:if test="count(*[3]/*) > 1">
-		<xsl:text>)</xsl:text>
-	</xsl:if>
-      </xsl:when>	
-
-	<!-- AXIOM -->
-	<xsl:when test="$name='Ax'">
-		<FONT color="blue">
-		<xsl:text>Ax</xsl:text>
-		</FONT>
-      	</xsl:when>
-	
-	<!-- VOID -->
-	<xsl:when test="$name='void'">
-		<FONT color="blue">
-		<xsl:text>Void</xsl:text>
-		</FONT>
-      	</xsl:when>	
-	
-	<!-- ATOM -->
-	<xsl:when test="$name='atom'">
-		<FONT color="blue">
-		<xsl:text>Atom</xsl:text>
-		</FONT>
-      	</xsl:when>	
-
-	
-	
-     <!-- FORALL -->
-     <xsl:when test="$name='forall'">
-       <xsl:choose>
-       <xsl:when test="$charlength > $framewidth">
-	<!-- &#x03a0; -->
-         <xsl:call-template name="mksymbol">
-          <xsl:with-param name="symbol" select="$forall"/>
-          <xsl:with-param name="color" select="'blue'"/>
-          <xsl:with-param name="size" select="'+2'"/>
-         </xsl:call-template>
-         <xsl:apply-templates select="m:bvar/m:ci">
-	 <xsl:with-param name="current_indent" select="$current_indent"/>
-         </xsl:apply-templates>
-         <xsl:text>:</xsl:text>
-         <xsl:apply-templates select="m:bvar/m:type">
-          <xsl:with-param name="current_indent" 
-           select="$current_indent + 5 + 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>
-        <xsl:apply-templates mode="inline" select="."/>
-       </xsl:otherwise>
-       </xsl:choose>
-      </xsl:when>
-
-      <!-- PRODUCT -->
-      <xsl:when test="$name='product'">
-       <xsl:choose>
-       <xsl:when test="$charlength > $framewidth">
-         <xsl:call-template name="mksymbol">
-          <xsl:with-param name="symbol" select="$product"/>
-          <xsl:with-param name="color" select="'blue'"/>
-          <xsl:with-param name="size" select="'+2'"/>
-         </xsl:call-template>
-         <xsl:apply-templates select="m:bvar/m:ci">
-	  <xsl:with-param name="current_indent" select="$current_indent"/>
-         </xsl:apply-templates>
-         <xsl:text>:</xsl:text>
-         <xsl:apply-templates select="m:bvar/m:type">
-          <xsl:with-param name="current_indent" 
-           select="$current_indent + 5 + 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>
-        <xsl:apply-templates mode="inline" select="."/>
-       </xsl:otherwise>
-       </xsl:choose>
-      </xsl:when>
-      
-       <!-- PROD_IND -->
-      <xsl:when test="$name='product_ind'">
-       <xsl:choose>
-       <xsl:when test="$charlength > $framewidth">
-       <FONT color="blue">
-     		<xsl:text>( </xsl:text>
-     	</FONT>
-         <xsl:apply-templates select="m:type">
-          <xsl:with-param name="current_indent" 
-           select="$current_indent + 5 + 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>
-	<FONT color="blue" size="+1">
-         <xsl:text> x </xsl:text>
-	 </FONT>
-         <xsl:apply-templates select="*[position()=3]">
-          <xsl:with-param name="current_indent" select="$current_indent + 2"/>
-         </xsl:apply-templates>
-	 <FONT color="blue">
-     		<xsl:text> )</xsl:text>
-     	</FONT>
-       </xsl:when>
-       <xsl:otherwise>
-        <xsl:apply-templates mode="inline" select="."/>
-       </xsl:otherwise>
-       </xsl:choose>
-      </xsl:when>
-
-      <!-- PAIR -->
-	<xsl:when test="$name='pair'">
-		<xsl:choose>
-		<xsl:when test="$charlength > $framewidth">
-			<FONT color="blue" size="+1">
-   			<xsl:text>&lt;</xsl:text>
-			</FONT>
-			<xsl:apply-templates select="*[position()=2]">
-			 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
-       			</xsl:apply-templates>
-			<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:apply-templates select="*[position()=3]">	
-			 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
-       			</xsl:apply-templates>
-			<FONT color="blue" size="+1">
-   			<xsl:text>&gt;</xsl:text>
-			</FONT>
-		</xsl:when>
-		<xsl:otherwise>
-		 	<xsl:apply-templates mode="inline" select="."/>
-       		</xsl:otherwise>
-		</xsl:choose>
-	</xsl:when>
-
-	<!-- UNION -->	
-		<xsl:when test="$name='union'">
-		<xsl:choose>
-		<xsl:when test="$charlength > $framewidth">
-			<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 color="blue" size="+1">
-   			<xsl:text>+</xsl:text>
-			</FONT>
-			<xsl:apply-templates select="*[position()=3]">
-			 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
-       			</xsl:apply-templates>
-		</xsl:when>
-		<xsl:otherwise>
-		 	<xsl:apply-templates mode="inline" select="."/>
-       		</xsl:otherwise>
-		</xsl:choose>
-	</xsl:when>
-	
-     <!-- INL -->
-     	<xsl:when test="$name='inl'">
-		<xsl:choose>
-		<xsl:when test="$charlength > $framewidth">
-			<FONT color="blue">
-   			<xsl:text>inl (</xsl:text>
-			</FONT>
-			<xsl:apply-templates select="*[position()=2]">
-			 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
-       			</xsl:apply-templates>
-			<FONT color="blue">
-   			<xsl:text> )</xsl:text>
-			</FONT>
-		</xsl:when>
-		<xsl:otherwise>
-		 	<xsl:apply-templates mode="inline" select="."/>
-       		</xsl:otherwise>
-		</xsl:choose>
-	</xsl:when>
-
-	<!-- INR -->
-     	<xsl:when test="$name='inr'">
-		<xsl:choose>
-		<xsl:when test="$charlength > $framewidth">
-			<FONT color="blue" size="+1">
-   			<xsl:text>inr (</xsl:text>
-			</FONT>
-			<xsl:apply-templates select="*[position()=2]">
-			 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
-       			</xsl:apply-templates>
-			<FONT color="blue" size="+1">
-   			<xsl:text> )</xsl:text>
-			</FONT>
-		</xsl:when>
-		<xsl:otherwise>
-		 	<xsl:apply-templates mode="inline" select="."/>
-       		</xsl:otherwise>
-		</xsl:choose>
-	</xsl:when>
-
-	<!-- PROP -->
-	<xsl:when test="$name='prop'">
-		<FONT color="blue">
-		<xsl:text>P</xsl:text>
-		</FONT>
-		<FONT color="blue" size="-2"> 
-		<xsl:apply-templates select="m:cn">
-		 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
-       	        </xsl:apply-templates>
-		</FONT>
-	</xsl:when>
-
-	<!-- UNIVERSE -->
-	<xsl:when test="$name='universe'">
-		<FONT color="blue" size="+1">
-		<xsl:text>U</xsl:text>
-		</FONT>
-		<FONT color="blue" size="2"> 
-		<xsl:apply-templates select="m:cn"/>
-		</FONT>
-	</xsl:when>
-
-	<!-- EQUAL -->
-	<xsl:when test="$name='equal'">
-       		<xsl:choose>
-       			<xsl:when test="$charlength > $framewidth">
-			<xsl:apply-templates select="*[position()=3]">
-			 <xsl:with-param name="current_indent" select="$current_indent"/> 
-       			</xsl:apply-templates>
-			<br/>
-			<xsl:call-template name="make_indent">
-        		 <xsl:with-param name="current_indent" select="$current_indent"/> 
-       			</xsl:call-template>
-			<FONT color="blue" size="+1">
-			 <xsl:text>= </xsl:text>
-			</FONT>
-       			<xsl:apply-templates select="*[position()=4]">
-        		 <xsl:with-param name="current_indent" select="$current_indent"/>
-       			</xsl:apply-templates>
-       			<br/>
-       			<xsl:call-template name="make_indent">
-        		<xsl:with-param name="current_indent" select="$current_indent"/> 
-       			</xsl:call-template>
-       			<!-- member -->
-       			<xsl:call-template name="mksymbol">
-        		<xsl:with-param name="symbol" select="$member"/>
-        		<xsl:with-param name="color" select="'blue'"/>
-        		<xsl:with-param name="size" select="'+0'"/>
-       			</xsl:call-template>
-       			<xsl:apply-templates select="*[position()=2]">
-        		<xsl:with-param name="current_indent" select="$current_indent"/>
-       			</xsl:apply-templates>
-       		</xsl:when>
-       		<xsl:otherwise>
-        		<xsl:apply-templates mode="inline" select="."/>
-       		</xsl:otherwise>
-       </xsl:choose>
-      </xsl:when>
-
-	<!-- TOKEN -->
-
-	<xsl:when test="$name='token'">
-		<FONT color="blue">
-		<xsl:text>"</xsl:text>
-		</FONT> 
-		<xsl:apply-templates select="m:ci"/>
-		<FONT color="blue">
-		<xsl:text>"</xsl:text>
-		</FONT> 
-	</xsl:when>
-
-	<!-- NIL -->
-
-	<xsl:when test="$name='nil'">
-		<FONT color="blue">
-		<xsl:text>[]</xsl:text>
-		</FONT> 
-	</xsl:when>
-
-	<!-- CONS -->
-	<xsl:when test="$name='cons'">
-		<xsl:apply-templates select="*[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 color="blue">
-		<xsl:text>::</xsl:text>
-		</FONT>
-		<xsl:apply-templates select="*[3]">
-		 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
-       		</xsl:apply-templates>
-	</xsl:when>
-	
-	
-	<!-- REC --> 
-
-	<xsl:when test="$name='rec'">
-		<xsl:choose>
-		<xsl:when test="$charlength > $framewidth">
-		<FONT color="blue">
-		<xsl:text>rectype</xsl:text>
-		</FONT>
-		<xsl:apply-templates select="*[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 color="blue">
-		<xsl:text>=</xsl:text>
-		</FONT>
-		<xsl:apply-templates select="*[3]">
-		 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
-       		</xsl:apply-templates>
-		</xsl:when>
-		<xsl:otherwise>
-        		<xsl:apply-templates mode="inline" select="."/>
-       		</xsl:otherwise>
-       		</xsl:choose>
-	</xsl:when>
-
-	<!-- SET -->
-
-	<xsl:when test="$name='t_set'">
-	<xsl:choose>
-		<xsl:when test="$charlength > $framewidth">
-		<FONT color="blue">
-		<xsl:text>{</xsl:text>
-		</FONT>
-		<xsl:choose>
-		<xsl:when test="m:bvar/m:ci">
-			<xsl:apply-templates select="m:bvar/m:ci"/>
-			<FONT color="blue">
-				<xsl:text>:</xsl:text>
-			</FONT>
-			<xsl:apply-templates select="m:bvar/m:type">
-				<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:when>
-		<xsl:otherwise>
-			<xsl:apply-templates select="m:bvar/m:type">
-				<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:otherwise>
-		</xsl:choose>
-		<FONT color="blue">
-			<xsl:text>|</xsl:text>
-		</FONT>
-		<xsl:apply-templates select="*[3]">
-		 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
-       		</xsl:apply-templates>
-
-		<FONT color="blue">
-			<xsl:text>}</xsl:text>
-		</FONT>
-
-		</xsl:when>
-		<xsl:otherwise>
-        		<xsl:apply-templates mode="inline" select="."/>
-       		</xsl:otherwise>
-       		</xsl:choose>
-	</xsl:when>
-
-  	<!-- ISECT -->
-
-	<xsl:when test="$name='isect'">
-		<xsl:call-template name="mksymbol">
-        	<xsl:with-param name="symbol" select="$intersection"/>
-        	<xsl:with-param name="color" select="'blue'"/>
-        	<xsl:with-param name="size" select="'+0'"/>
-       		</xsl:call-template>
-		<xsl:apply-templates select="m:bvar/m:ci"/>
-		<FONT color="blue">
-		<xsl:text>:</xsl:text>
-		</FONT>
-		<xsl:apply-templates select="m:bvar/m:type">
-		<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 color="blue">
-		<xsl:text>.</xsl:text>
-		</FONT>
-		<xsl:apply-templates select="*[3]">
-	       	 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
-       		</xsl:apply-templates>
-
-	</xsl:when>
-
-	<!-- QUOTIENT --> 
-
-	<xsl:when test="$name='quotient'">
-		<xsl:apply-templates select="m:bvar[1]"/>
-		<xsl:text>,</xsl:text>
-		<xsl:apply-templates select="m:bvar[2]"/>
-		<FONT color="blue">
-		<xsl:text>:</xsl:text>
-		</FONT>
-		<xsl:apply-templates select="*[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 color="blue">
-		<xsl:text>//</xsl:text>
-		</FONT>
-		<xsl:apply-templates select="*[5]">
-		 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
-       		</xsl:apply-templates>
-
-	</xsl:when>
-
-	<!-- IF_THEN_ELSE -->
-	<xsl:when test="$name='if_then_else'">
-		<xsl:choose>
-		<xsl:when test="m:where = 'atom_eq'">
-			<FONT color="blue">
-			<xsl:text>atom_eq (</xsl:text>
-			</FONT>
-		</xsl:when>
-		<xsl:when test="m:where = 'int_eq'">
-			<FONT color="blue">
-			<xsl:text>int_eq (</xsl:text>
-			</FONT>
-		</xsl:when>
-		<xsl:when test="m:where = 'less'">
-			<FONT color="blue">
-			<xsl:text>less (</xsl:text>
-			</FONT>
-		</xsl:when>
-		</xsl:choose>
-		<xsl:apply-templates select="*[3]"/>
-		<xsl:text>; </xsl:text>
-		<xsl:apply-templates select="*[4]"/>
-		<xsl:text>; </xsl:text>
-		<xsl:apply-templates select="*[5]"/>
-		<xsl:text>; </xsl:text>	
-		<xsl:apply-templates select="*[6]"/>
-		<FONT color="blue">
-		<xsl:text>)</xsl:text>
-		</FONT>
-	</xsl:when>
-
-
-	<!-- SO_LAMBDA -->
-	<xsl:when test="$name='so_lambda'">
-     	<xsl:choose>
-     		<xsl:when test="$charlength > $framewidth">
-       			<xsl:call-template name="mksymbol">
-        			<xsl:with-param name="symbol" select="$lambda"/>
-        			<xsl:with-param name="color" select="'red'"/>
-        			<xsl:with-param name="size" select="'+2'"/>
-       			</xsl:call-template>
-       			<xsl:apply-templates select="m:apply[1]/*[2]"/>
-       			<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="*[3]">
-        		 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
-       			</xsl:apply-templates>
-     		</xsl:when>
-     		<xsl:otherwise>
-      			<xsl:apply-templates mode="inline" select="."/>
-     		</xsl:otherwise>
-     </xsl:choose>
-     </xsl:when>
-
-
-	<!-- SO_APPLY -->
-
-	<xsl:when test="$name='so_apply'">
-	<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:apply-templates mode="inline" select="."/>
-       </xsl:otherwise>
-       </xsl:choose>
-      </xsl:when>
-      
-      <!-- APP -->
-      <xsl:when test="$name='app'">
-       	<xsl:choose>
-       	<xsl:when test="$charlength  > $framewidth">
-         <!-- NuPRL rendering -->
-         <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:if test="count(*) &gt; 2">
-          <xsl:text>(</xsl:text>
-          <xsl:for-each select="*[position() &gt; 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="." mode="inline"/>
-           <xsl:if test="not(position() = last())">
-            <xsl:text>,</xsl:text>
-           </xsl:if>
-          </xsl:for-each>
-          <xsl:text>)</xsl:text>
-         </xsl:if>
-                <!-- CIC rendering
-        	<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:apply-templates mode="inline" select="."/>
-       </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:apply-templates mode="inline" select="."/>
-          </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>
-         <br/>
-         <xsl:call-template name="make_indent">
-          <xsl:with-param name="current_indent" select="$current_indent + 2"/>           </xsl:call-template>
-         <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="m:piecewise/m:piece">
-    <!--   <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="./*[2]"/>
-            <xsl:call-template name="mksymbol">
-             <xsl:with-param name="symbol" select="$RightArrow"/>
-             <xsl:with-param name="color" select="'green'"/>
-             <xsl:with-param name="size" select="'+0'"/>
-            </xsl:call-template>
-            <xsl:variable name="body_size">
-  <xsl:apply-templates 
-              select="./*[1]/*[1]" mode="charcount"/>
-            </xsl:variable>
-            <xsl:choose>
-             <xsl:when test="$body_size > $framewidth">
-              <br/>
-              <xsl:call-template name="make_indent">
-               <xsl:with-param name="current_indent" 
-                    select="$current_indent + 8"/>   
-              </xsl:call-template>
-<xsl:apply-templates 
-                   select="./*[1]">
-              <xsl:with-param name="current_indent" 
-                   select="$current_indent + 8"/>      
-             </xsl:apply-templates>
-            </xsl:when>
-            <xsl:otherwise>
-     <xsl:apply-templates select="./*[1]"
-                   mode="inline" />
-            </xsl:otherwise>
-           </xsl:choose>
-         </xsl:for-each>
-       </xsl:when>
-       <xsl:otherwise>
-        <xsl:apply-templates mode="inline" select="."/> 
-       </xsl:otherwise>
-       </xsl:choose>
-      </xsl:when>
-      <!-- FIX -->
-      <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:apply-templates mode="inline" select="."/>
-       </xsl:otherwise>
-       </xsl:choose>
-      </xsl:when> 
-      <!-- COFIX -->
-      <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:apply-templates mode="inline" select="m:type"/>
-       </xsl:otherwise>
-       </xsl:choose>
-      </xsl:when>
-      <xsl:when test="$name='let_in'">
-       <xsl:text>let&#x00a0;</xsl:text>
-       <xsl:apply-templates select="m:bvar/m:ci"/>
-       <xsl:text>&#x00a0;:=&#x00a0;</xsl:text>
-       <xsl:apply-templates select="*[3]">
-        <xsl:with-param name="current_indent" select="$current_indent+14"/>
-       </xsl:apply-templates>
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:call-template>
-       <xsl:text>in&#x00a0;</xsl:text>
-       <xsl:apply-templates select="*[4]">
-        <xsl:with-param name="current_indent" select="$current_indent+5"/>
-       </xsl:apply-templates>
-      </xsl:when>
-
-      <!-- ***************************************** -->
-      <!-- *********** PROOF ELEMENTS ************** -->
-      <!-- ***************************************** -->
-      <!-- PROOF -->
-      <xsl:when test="$name='proof'">
-       <xsl:variable name="nonce" select="generate-id()"/>
-       <xsl:variable name="freshid1" select="concat('a',$nonce)"/>
-       <xsl:variable name="freshid2" select="concat('b',$nonce)"/>
-       <xsl:variable name="freshid3" select="concat('c',$nonce)"/>
-       <span ID="{$freshid1}">
-        <xsl:apply-templates select="*[position()=2]">
-         <xsl:with-param name="current_indent" select="$current_indent"/>
-        </xsl:apply-templates>
-        &#x00a0;
-       </span>
-       <xsl:choose>
-        <xsl:when test="(preceding-sibling::*[1]/text()='letin1') or
-                        (preceding-sibling::*[1]/text()='rw_step') or
-                        (name(..)='m:lambda')">
-         <br/>
-         <xsl:call-template name="make_indent">
-          <xsl:with-param name="current_indent" select="$current_indent"/>
-         </xsl:call-template>
-         <FONT color="red">we proved&#x00a0;</FONT> 
-        </xsl:when>
-        <xsl:otherwise>
-         <script>
-          if(document.getElementById) {
-           document.write('\
-            <span ID="{$freshid2}">\
-             <a style="text-decoration:underline ; color:green" href="" onClick="Show(document.getElementById(\'{$freshid1}\')); Hide(document.getElementById(\'{$freshid2}\'));Show(document.getElementById(\'{$freshid3}\'));return (0==1);">Proof of</a>\
-            </span>\
-            <span ID="{$freshid3}">\
-             <br/>\
-             <xsl:call-template name="make_indent">
-              <xsl:with-param name="current_indent" select="$current_indent"/>
-             </xsl:call-template>\
-             <a style="text-decoration:underline ; color:red" href="" onClick="Hide(document.getElementById(\'{$freshid1}\')); Show(document.getElementById(\'{$freshid2}\'));Hide(document.getElementById(\'{$freshid3}\'));return (0==1);">we proved</a>\
-            </span>\
-           ');
-           document.to_be_deleted.push('<xsl:value-of select="$freshid1"/>');
-           document.to_be_deleted.push('<xsl:value-of select="$freshid3"/>');
-           document.write('&#x00a0;');
-          } else {
-           document.write('\
-            <br/>\
-            <xsl:call-template name="make_indent">
-             <xsl:with-param name="current_indent" select="$current_indent"/>
-            </xsl:call-template>\
-            <FONT color="red">we proved&#x00a0;</FONT>\
-           ');
-          }
-         </script>
-        </xsl:otherwise>
-       </xsl:choose>
-       <xsl:apply-templates select="*[position()=3]">
-        <xsl:with-param name="current_indent" select="$current_indent + 16"/>
-       </xsl:apply-templates>
-      </xsl:when>
-      <!-- side_proof -->
-      <xsl:when test="$name='side_proof'">
-       <xsl:variable name="nonce" select="generate-id()"/>
-       <xsl:variable name="freshid1" select="concat('a',$nonce)"/>
-       <xsl:variable name="freshid2" select="concat('b',$nonce)"/>
-       <xsl:variable name="freshid3" select="concat('c',$nonce)"/>
-       <xsl:variable name="freshid4" select="concat('d',$nonce)"/>
-       <span ID="{$freshid1}">
-        <xsl:apply-templates select="*[position()=2]">
-         <xsl:with-param name="current_indent" select="$current_indent"/>
-        </xsl:apply-templates>
-        &#x00a0;
-       </span>
-         <script>
-          if(document.getElementById) {
-           document.write('\
-            <span ID="{$freshid2}">\
-             <a style="text-decoration:underline ; color:green" href="" onClick="Show(document.getElementById(\'{$freshid1}\')); Hide(document.getElementById(\'{$freshid2}\'));Show(document.getElementById(\'{$freshid3}\'));Show(document.getElementById(\'{$freshid4}\'));return (0==1);">Justification</a>\
-            </span>\
-            <span ID="{$freshid3}">\
-             <br/>\
-             <xsl:call-template name="make_indent">
-              <xsl:with-param name="current_indent" select="$current_indent"/>
-             </xsl:call-template>\
-             <a style="text-decoration:underline ; color:red" href="" onClick="Hide(document.getElementById(\'{$freshid1}\')); Show(document.getElementById(\'{$freshid2}\'));Hide(document.getElementById(\'{$freshid3}\'));Hide(document.getElementById(\'{$freshid4}\'));return (0==1);">we proved</a>\
-            </span>\
-           ');
-           document.to_be_deleted.push('<xsl:value-of select="$freshid1"/>');
-           document.to_be_deleted.push('<xsl:value-of select="$freshid3"/>');
-           document.to_be_deleted.push('<xsl:value-of select="$freshid4"/>');
-           document.write('&#x00a0;');
-          } else {
-           document.write('\
-            <br/>\
-            <xsl:call-template name="make_indent">
-             <xsl:with-param name="current_indent" select="$current_indent"/>
-            </xsl:call-template>\
-            <FONT color="red">we proved&#x00a0;</FONT>\
-           ');
-          }
-         </script>
-       <span ID="{$freshid4}">
-        <xsl:apply-templates select="*[position()=3]">
-         <xsl:with-param name="current_indent" select="$current_indent + 16"/>
-        </xsl:apply-templates>
-       </span>
-      </xsl:when> 
-      <!-- eq_chain -->
-      <xsl:when test="$name='eq_chain'">
-       <FONT color="red">We have the following equality chain:</FONT>
-       <xsl:for-each select="*[position() mod 2 = 0]">
-        <xsl:variable name="pos" select="position()"/>
-        <br/>
-        <xsl:call-template name="make_indent">
-         <xsl:with-param name="current_indent" select="$current_indent + 5"/>
-        </xsl:call-template>
-        <xsl:choose>
-         <xsl:when test="$pos=1">
-          <xsl:apply-templates select=".">
-           <xsl:with-param name="current_indent" select="$current_indent + 5"/>
-          </xsl:apply-templates>
-          <xsl:text>&#x00a0;=</xsl:text>
-         </xsl:when>
-         <xsl:otherwise>
-          <xsl:text>=&#x00a0;</xsl:text>
-          <xsl:apply-templates select=".">
-           <xsl:with-param name="current_indent" select="$current_indent + 5"/>
-          </xsl:apply-templates>
-         </xsl:otherwise>
-        </xsl:choose>
-        <xsl:if test="$pos != last()">
-         <br/>
-         <xsl:call-template name="make_indent">
-          <xsl:with-param name="current_indent" select="$current_indent + 15"/>
-         </xsl:call-template>
-         <xsl:apply-templates select="../*[position()=2*$pos +1]">
-          <xsl:with-param name="current_indent" select="$current_indent + 15"/>
-         </xsl:apply-templates>
-        </xsl:if>
-       </xsl:for-each>
-      </xsl:when>
-       <!-- diseq_chain -->
-      <xsl:when test="$name='diseq_chain'">
-       <FONT color="red">We have the following chain of disequalities:</FONT>
-       <xsl:for-each select="*[position() mod 3 = 2]">
-        <xsl:variable name="pos" select="position()"/>
-        <br/>
-        <xsl:call-template name="make_indent">
-         <xsl:with-param name="current_indent" select="$current_indent + 5"/>
-        </xsl:call-template>
-        <xsl:choose>
-         <xsl:when test="$pos=1">
-          <xsl:apply-templates select=".">
-           <xsl:with-param name="current_indent" select="$current_indent + 5"/>
-          </xsl:apply-templates>
-          <xsl:text>&#x00a0;</xsl:text>
-          <xsl:apply-templates mode="inline" select="../*[position()=3*$pos]"/>
-         </xsl:when>
-         <xsl:otherwise>
-          <xsl:apply-templates mode="inline" select="../*[position()=3*($pos - 1)]"/>
-          <xsl:text>&#x00a0;</xsl:text>
-          <xsl:apply-templates select=".">
-           <xsl:with-param name="current_indent" select="$current_indent + 5"/>
-          </xsl:apply-templates>
-         </xsl:otherwise>
-        </xsl:choose>
-        <xsl:if test="$pos != last()">
-         <br/>
-         <xsl:call-template name="make_indent">
-          <xsl:with-param name="current_indent" select="$current_indent + 15"/>
-         </xsl:call-template>
-         <xsl:apply-templates select="../*[position()=3*$pos +1]">
-          <xsl:with-param name="current_indent" select="$current_indent + 15"/>
-         </xsl:apply-templates>
-        </xsl:if>
-       </xsl:for-each>
-      </xsl:when>
-      <!-- letin1 -->
-      <xsl:when test="$name='letin1'">
-       <xsl:apply-templates select="*[position()=2]">
-        <xsl:with-param name="current_indent" select="$current_indent"/>
-       </xsl:apply-templates>
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:call-template>
-       <xsl:apply-templates select="*[position()=3]">
-        <xsl:with-param name="current_indent" select="$current_indent"/>
-       </xsl:apply-templates>
-      </xsl:when>
-      <!-- letin -->
-      <xsl:when test="$name='letin'">
-       <xsl:for-each select="*[position()>1 and last()>position()]">
-        <xsl:apply-templates select=".">
-         <xsl:with-param name="current_indent" select="$current_indent"/>
-        </xsl:apply-templates>
-        <br/>
-        <xsl:call-template name="make_indent">
-         <xsl:with-param name="current_indent" select="$current_indent"/> 
-        </xsl:call-template>
-       </xsl:for-each>
-       <xsl:apply-templates select="*[position()=last()]">
-        <xsl:with-param name="current_indent" select="$current_indent"/>
-       </xsl:apply-templates>
-      </xsl:when>
-      <!-- Let -->
-      <xsl:when test="$name='let'">
-       (
-       <xsl:apply-templates select="m:ci"/>
-       )
-       <xsl:apply-templates select="*[3]">
-        <xsl:with-param name="current_indent" select="$current_indent + 7"/>
-       </xsl:apply-templates>
-      </xsl:when>
-      <!-- rw_step -->
-      <xsl:when test="$name='rw_step'">
-       <xsl:choose>
-        <xsl:when test="name(*[2])='m:apply'">
-         <xsl:apply-templates select="*[2]">
-          <xsl:with-param name="current_indent" select="$current_indent"/>
-         </xsl:apply-templates>
-        </xsl:when>
-        <xsl:otherwise>
-         <FONT color="red">Consider&#x00a0;</FONT>
-         <xsl:apply-templates select="*[2]"/>
-        </xsl:otherwise>
-       </xsl:choose>
-       <xsl:variable name="charlength_first">
-        <xsl:apply-templates select="*[3]" mode="root_charcount"/>
-       </xsl:variable>
-       <xsl:variable name="charlength_second">
-        <xsl:apply-templates select="*[4]" mode="root_charcount"/>
-       </xsl:variable>
-       <xsl:variable name="charlength_side_proof">
-        <xsl:apply-templates select="*[5]" mode="root_charcount"/>
-       </xsl:variable>
-       <xsl:variable name="split1"
-         select="($charlength_first + $charlength_second) > $framewidth"/>
-       <xsl:variable name="split2"
-         select="($charlength_second + $charlength_side_proof) > $framewidth"/>
-     <!-- <xsl:value-of select="$current_indent"/> -->
-     <!-- <xsl:value-of select="string($charlength_second)"/>  -->
-     <!-- <xsl:value-of select="$charlength_side_proof"/>  -->
-     <!-- <xsl:value-of select="$split2"/>  -->
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:call-template>
-       <FONT color="red">Rewrite&#x00a0;</FONT>
-       <xsl:apply-templates mode="inline" select="*[3]"/>
-       <xsl:text>&#x00a0;</xsl:text>
-       <xsl:if test="$split1">
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
-       </xsl:call-template>
-       </xsl:if>
-       <FONT color="red">with&#x00a0;</FONT>
-       <xsl:apply-templates mode="inline" select="*[4]"/>
-       <xsl:text>&#x00a0;</xsl:text>
-       <xsl:if test="$split2">
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
-       </xsl:call-template>
-       </xsl:if>
-       <FONT color="red">by&#x00a0;</FONT>
-       <xsl:apply-templates select="*[5]">
-        <xsl:with-param name="current_indent" select="$current_indent+7"/>
-       </xsl:apply-templates>
-      </xsl:when>
-      <!-- rewrite and apply -->
-      <xsl:when test="$name='rewrite_and_apply'">
-       <xsl:apply-templates select="*[2]">
-        <xsl:with-param name="current_indent" select="$current_indent"/>
-       </xsl:apply-templates>
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:call-template>
-       <FONT color="red">Then apply it to&#x00a0;</FONT>
-       <xsl:apply-templates select="*[position()>2]"/>
-      </xsl:when>
-      <!-- by_induction -->
-      <xsl:when test="$name='by_induction'">
-       <FONT color="red">We prove&#x00a0;</FONT>
-       <xsl:apply-templates select="../*[3]">
-        <xsl:with-param name="current_indent" select="$current_indent+18"/>
-       </xsl:apply-templates>
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:call-template>
-       <FONT color="red">by induction on&#x00a0;</FONT>
-       <xsl:apply-templates select="*[position()=last()]/*[position()=last()]">
-        <xsl:with-param name="current_indent" select="$current_indent+30"/>
-       </xsl:apply-templates>
-       <!-- 
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:call-template>
-       <xsl:text>The induction property is</xsl:text>
-       <br/> 
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:call-template>
-       <xsl:apply-templates select="*[3]">
-        <xsl:with-param name="current_indent" select="$current_indent"/>
-       </xsl:apply-templates>
-       -->
-       <xsl:apply-templates 
-            select="*[position()>3 and not(position()=last())]">
-        <xsl:with-param name="current_indent" select="$current_indent+4"/>
-       </xsl:apply-templates>
-       <!-- <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:call-template>
-       <xsl:text>End induction</xsl:text> -->
-      </xsl:when>
-      <!-- inductive_case -->
-      <xsl:when test="$name='inductive_case'">
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:call-template>
-       <FONT color="red">Case&#x00a0;</FONT>
-       <xsl:apply-templates select="*[2]">
-        <xsl:with-param name="current_indent" select="$current_indent +10"/>
-       </xsl:apply-templates>
-       <xsl:if test="*[3]/*[position()>1]">
-        <br/>
-        <xsl:call-template name="make_indent">
-         <xsl:with-param name="current_indent" select="$current_indent+4"/> 
-        </xsl:call-template>
-        <FONT color="red">By induction hypothesis, we have:</FONT>
-        <xsl:for-each select="*[3]/*[position()>1]">
-         <br/>
-         <xsl:call-template name="make_indent">
-          <xsl:with-param name="current_indent" select="$current_indent + 4"/> 
-         </xsl:call-template>
-         <xsl:text>(</xsl:text>
-         <xsl:apply-templates select="m:ci"/>
-         <xsl:text>)&#x00a0;</xsl:text>
-         <xsl:apply-templates select="m:type">
-          <xsl:with-param name="current_indent" select="$current_indent + 8"/>
-         </xsl:apply-templates>
-        </xsl:for-each>
-       </xsl:if>
-       <br/>
-        <xsl:call-template name="make_indent">
-         <xsl:with-param name="current_indent" select="$current_indent + 4"/> 
-        </xsl:call-template>
-       <xsl:apply-templates select="*[4]">
-        <xsl:with-param name="current_indent" select="$current_indent +4"/>
-       </xsl:apply-templates>
-       <!-- <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:call-template>
-       <xsl:text>End Case</xsl:text> -->
-      </xsl:when>
-      <!-- case_lhs  -->
-      <xsl:when test="$name='case_lhs'">
-       <xsl:choose>
-        <xsl:when test="count(*)=2">
-         <xsl:apply-templates mode="inline" select="*[2]"/>
-        </xsl:when>
-        <xsl:otherwise>
-         <xsl:text>(</xsl:text>
-         <xsl:apply-templates mode="inline" select="*[2]"/>
-         <xsl:for-each select="m:bvar">
-          <xsl:text>&#x00a0;</xsl:text>
-          <xsl:apply-templates mode="inline" select="*[1]"/>
-          <xsl:text>:</xsl:text>
-          <xsl:apply-templates mode="inline" select="m:type/*[1]"/>
-         </xsl:for-each>
-         <xsl:text>)</xsl:text>
-        </xsl:otherwise>
-       </xsl:choose>
-      </xsl:when>
-      <!-- false_ind -->
-      <xsl:when test="$name='false_ind'">
-       <xsl:apply-templates select="*[3]">
-        <xsl:with-param name="current_indent" select="$current_indent"/>
-       </xsl:apply-templates> 
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:call-template> 
-       <FONT color="red">Contradiction.</FONT>
-      </xsl:when>
-      <!-- and_ind -->
-      <xsl:when test="$name='and_ind'">
-       <xsl:choose>
-        <xsl:when test="name(*[2])='m:apply'">
-         <xsl:apply-templates select="*[2]">
-          <xsl:with-param name="current_indent" select="$current_indent"/>
-         </xsl:apply-templates>      
-        </xsl:when>
-        <xsl:otherwise>
-         <FONT color="red">Consider&#x00a0;</FONT>
-         <xsl:apply-templates select="*[2]"/>
-        </xsl:otherwise>
-       </xsl:choose>
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:call-template>
-       <FONT color="red">In particular, we have</FONT>
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:call-template>
-       (
-       <xsl:apply-templates select="*[3]"/>
-       )&#x00a0;
-       <xsl:apply-templates select="*[4]">
-        <xsl:with-param name="current_indent" select="$current_indent + 9"/> 
-       </xsl:apply-templates>
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:call-template>
-       (
-       <xsl:apply-templates select="*[5]"/>
-       )&#x00a0;
-       <xsl:apply-templates select="*[6]">
-        <xsl:with-param name="current_indent" select="$current_indent + 9"/> 
-       </xsl:apply-templates>
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:call-template>
-       <xsl:apply-templates select="*[7]">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:apply-templates>
-      </xsl:when>
-      <!-- full_or_ind -->
-      <xsl:when test="$name='full_or_ind'">
-       <xsl:choose>
-        <xsl:when test="name(*[2])='m:apply'">
-         <xsl:apply-templates select="*[2]">
-          <xsl:with-param name="current_indent" select="$current_indent"/> 
-         </xsl:apply-templates>
-        </xsl:when>
-        <xsl:otherwise>
-         <FONT color="red">Consider&#x00a0;</FONT>
-         <xsl:apply-templates select="*[2]"/>
-        </xsl:otherwise>
-       </xsl:choose>
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:call-template>
-       <FONT color="red">We proceed by cases to prove&#x00a0;</FONT>
-       <xsl:apply-templates select="*[3]"/>
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent+4"/> 
-       </xsl:call-template>
-       <FONT color="red">Left: suppose&#x00a0;</FONT>
-       <xsl:text>(</xsl:text>
-       <xsl:value-of select="*[4]/m:bvar/m:ci"/>
-       <xsl:text>)&#x00a0;</xsl:text>
-       <xsl:apply-templates 
-            select="*[4]/m:bvar/m:type/*[1]"/>
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent+15"/> 
-       </xsl:call-template>
-       <xsl:apply-templates 
-            select="*[4]/*[3]">
-        <xsl:with-param name="current_indent" select="$current_indent+15"/>
-       </xsl:apply-templates>
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent+4"/> 
-       </xsl:call-template>
-       <FONT color="red">Right: suppose&#x00a0;</FONT>
-       <xsl:text>(</xsl:text>
-       <xsl:value-of select="*[5]/m:bvar/m:ci"/>
-       <xsl:text>)&#x00a0;</xsl:text>
-       <xsl:apply-templates 
-            select="*[5]/m:bvar/m:type/*[1]"/>
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent+16"/> 
-       </xsl:call-template>
-       <xsl:apply-templates 
-            select="*[5]/*[3]">
-        <xsl:with-param name="current_indent" select="$current_indent+16"/>
-       </xsl:apply-templates>
-      </xsl:when>
-      <!-- or_ind -->
-      <xsl:when test="$name='or_ind'">
-       <xsl:choose>
-        <xsl:when test="name(*[2])='m:apply'">
-         <xsl:apply-templates select="*[2]">
-          <xsl:with-param name="current_indent" select="$current_indent"/> 
-         </xsl:apply-templates>
-        </xsl:when>
-        <xsl:otherwise>
-         <FONT color="red">Consider&#x00a0;</FONT>
-         <xsl:apply-templates select="*[2]"/>
-        </xsl:otherwise>
-       </xsl:choose>
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:call-template>
-       <FONT color="red">We prove&#x00a0;</FONT>
-       <xsl:apply-templates select="*[3]"/>
-       <FONT color="red">&#x00a0;by cases:</FONT>
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:call-template>
-       Left:&#x00a0;
-       <xsl:apply-templates select="*[4]">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:apply-templates>
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:call-template>
-       Right:&#x00a0;
-       <xsl:apply-templates select="*[5]">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:apply-templates>
-      </xsl:when>
-      <!-- Ex_ind -->
-      <xsl:when test="$name='ex_ind'">
-       <xsl:choose>
-        <xsl:when test="name(*[2])='m:apply'">
-         <xsl:apply-templates select="*[2]">
-          <xsl:with-param name="current_indent" select="$current_indent"/>
-         </xsl:apply-templates>
-        </xsl:when>
-        <xsl:otherwise>
-         <FONT color="red">Consider&#x00a0;</FONT>
-         <xsl:apply-templates select="*[2]">
-          <xsl:with-param name="current_indent" select="$current_indent"/>
-         </xsl:apply-templates>
-        </xsl:otherwise>
-       </xsl:choose>
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:call-template>
-       <FONT color="red">Let&#x00a0;</FONT>
-       <xsl:apply-templates mode="inline" select="*[3]"/>
-       :
-       <xsl:apply-templates mode="inline" select="*[4]"/>
-       <FONT color="red">&#x00a0;such that</FONT>
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:call-template>
-       (
-       <xsl:apply-templates mode="inline" select="*[5]"/>
-       )
-       <xsl:apply-templates select="*[6]">
-        <xsl:with-param name="current_indent" select="$current_indent +7"/>
-       </xsl:apply-templates>
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:call-template>
-       <xsl:apply-templates select="*[7]">
-        <xsl:with-param name="current_indent" select="$current_indent"/>
-       </xsl:apply-templates>
-      </xsl:when>
-     </xsl:choose>
-</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:value-of select="$current_indent"/> -->
-     <xsl:choose>
-     <xsl:when test="$charlength > $framewidth">
-       <!-- &#x03bb; -->
-       <xsl:call-template name="mksymbol">
-        <xsl:with-param name="symbol" select="$lambda"/>
-        <xsl:with-param name="color" select="'red'"/>
-        <xsl:with-param name="size" select="'+2'"/>
-       </xsl:call-template>
-       <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 + 4 + 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>
-      <xsl:apply-templates mode="inline" select="."/>
-     </xsl:otherwise>
-     </xsl:choose>
-</xsl:template>
-
-<!-- href -->
-<xsl:template match="m:ci">
- <xsl:choose>
-  <xsl:when test="boolean(@definitionURL)">
-   <a href="{@definitionURL}">
-   <xsl:apply-templates/>
-   </a>
-  </xsl:when>
-  <xsl:otherwise>
-   <xsl:value-of select="."/>
-  </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
-
-<!-- CHAR COUNTING -->
-
-<!-- enter this counting mode selecting the root -->
-<xsl:template match="*" mode="root_charcount">
-<xsl:param name="incurrent_length" select="0"/>
- <xsl:choose>
-  <xsl:when test="count(*)=0">
-   <xsl:value-of select="0"/>
-  </xsl:when>
-  <xsl:when test="name()='m:ci'">
-   <xsl:value-of select="string-length()"/>
-  </xsl:when>
-  <xsl:otherwise>
-   <xsl:apply-templates select="*[1]" mode="charcount">
-    <xsl:with-param name="incurrent_length" select="$incurrent_length"/>
-   </xsl:apply-templates>
-  </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
-
-
-	<!-- CASI PARTICOLARI MODE=INLINE -->
-
-<xsl:template mode="inline" match="m:interval">
-	<FONT color="blue">
-	<xsl:text>[</xsl:text>
-	</FONT>
-	<xsl:apply-templates select="*[1]"/>
-	<xsl:text>, </xsl:text>
-	<xsl:apply-templates select="*[2]"/>
-	<FONT color="blue">
-	<xsl:text>]</xsl:text>
-	</FONT>
-</xsl:template>
-
-<xsl:template mode="inline" match="m:apply[m:in]">
-	<xsl:apply-templates select="*[2]"/>
-	<xsl:text> </xsl:text>
-	<xsl:call-template name="mksymbol">
-        	<xsl:with-param name="symbol" select="$member"/>
-        	<xsl:with-param name="color" select="'blue'"/>
-        	<xsl:with-param name="size" select="'+0'"/>
-       	</xsl:call-template>
-	<xsl:text> </xsl:text>
-	<xsl:apply-templates select="*[3]"/>
-</xsl:template>
-
-<xsl:template mode="inline" match="m:integers">
-	<xsl:call-template name="mksymbol">
-        	<xsl:with-param name="symbol" select="$integers"/>
-        	<xsl:with-param name="color" select="'blue'"/>
-        	<xsl:with-param name="size" select="'+0'"/>
-       	</xsl:call-template>
-</xsl:template>
-
-<xsl:template mode="inline" match="m:naturalnumbers">
-	<xsl:call-template name="mksymbol">
-        	<xsl:with-param name="symbol" select="$naturalnumbers"/>
-        	<xsl:with-param name="size" select="'+0'"/>
-       	</xsl:call-template>
-</xsl:template>
-
-<xsl:template mode="inline" match="m:apply[m:implies]">
-	<xsl:text>(</xsl:text>
-	<xsl:apply-templates select="*[2]"/>
-	<xsl:text> </xsl:text>
-	<xsl:call-template name="mksymbol">
-        	<xsl:with-param name="symbol" select="$implies"/>
-        	<xsl:with-param name="color" select="'blue'"/>
-        	<xsl:with-param name="size" select="'+0'"/>
-       	</xsl:call-template>
-	<xsl:text> </xsl:text>
-	<xsl:apply-templates select="*[3]"/>
-	<xsl:text>)</xsl:text>
-</xsl:template>
-
-<xsl:template mode="inline" match="m:apply[m:exists]">
-               <xsl:call-template name="mksymbol">
-		<xsl:with-param name="symbol" select="$NUPRLexists"/>
-        	<xsl:with-param name="color" select="'blue'"/>
-		<xsl:with-param name="size" select="'+0'"/>
-	</xsl:call-template>
-	<xsl:apply-templates select="m:bvar/m:ci"/>
-     	<xsl:text>:</xsl:text>
-         <xsl:apply-templates select="m:condition/*"/>
-<!-- CSC: old wrong code
-     	<xsl:if test="count(m:condition/m:apply/*[3]) > 1">
-     		<xsl:text>(</xsl:text>
-     	</xsl:if>
-     	<xsl:apply-templates select="m:condition/m:apply/*[3]"/>
-     	<xsl:if test="count(m:bvar/m:type/m:apply/*[3]) > 1">
-     		<xsl:text>)</xsl:text>
-     	</xsl:if>
--->
-     	<xsl:text>.</xsl:text>
-     	<xsl:apply-templates select="*[position()=4]"/>
-
-
-</xsl:template>
-<!--
-<xsl:template mode="inline" match="m:apply/*[m:ci][position()=1]">
-	<xsl:apply-templates select="*[1]"/>
-	<xsl:text>(</xsl:text>
-	<xsl:for-each select="*[position()>1 and position()!=last()]">
-		<xsl:apply-templates/>
-		<xsl:text>, </xsl:text>
-	</xsl:for-each>
-	<xsl:apply-templates select="*[position()=last()]"/>
-	<xsl:text>)</xsl:text>
-</xsl:template>
--->
-<!-- CASI PARTICOLARI NON IN LINE -->
-
-<xsl:template match="m:interval">
-	<FONT color="blue">
-	<xsl:text>[</xsl:text>
-	</FONT>
-	<xsl:apply-templates select="*[1]"/>
-	<xsl:text>, </xsl:text>
-	<xsl:apply-templates select="*[2]"/>
-	<FONT color="blue">
-	<xsl:text>]</xsl:text>
-	</FONT>
-
-
- <!--<xsl:param name="current_indent" select="0"/>
-        <xsl:variable name="charlength">
-	 <xsl:apply-templates select="." mode="charcount"/>
-	</xsl:variable>
-	<xsl:choose>
-	<xsl:when test="$charlength > $framewidth">
-	<FONT color="blue">
-	<xsl:text>[</xsl:text>
-	</FONT>
-	<xsl:apply-templates select="*[1]">
-	 <xsl:with-param name="current_indent" select="$current_indent"/> 
-	</xsl:apply-templates>
-	<xsl:text>, </xsl:text>
-	<br/>
-	<xsl:call-template name="make_indent">
- 	 <xsl:with-param name="current_indent" select="$current_indent"/> 
-        </xsl:call-template>
-	<xsl:apply-templates select="*[2]">
-	 <xsl:with-param name="current_indent" select="$current_indent"/> 
-	</xsl:apply-templates>
-	<FONT color="blue">
-	<xsl:text>]</xsl:text>
-	</FONT>
-	</xsl:when>
-	<xsl:otherwise>
-	</xsl:otherwise>
-	</xsl:choose>-->
-</xsl:template>
-
-<xsl:template match="m:apply[m:in]">
- <xsl:param name="current_indent" select="0"/>
-	<xsl:variable name="charlength">
-	 <xsl:apply-templates select="m:in" mode="charcount"/>
-	</xsl:variable>
-	<xsl:choose>
-	<xsl:when test="$charlength > $framewidth">
-	<xsl:apply-templates select="*[2]">
-	 <xsl:with-param name="current_indent" select="$current_indent"/> 
-	</xsl:apply-templates>
-	<br/>
-	<xsl:call-template name="make_indent">
- 	 <xsl:with-param name="current_indent" select="$current_indent"/> 
-        </xsl:call-template>
-	<xsl:call-template name="mksymbol">
-        	<xsl:with-param name="symbol" select="$member"/>
-        	<xsl:with-param name="color" select="'blue'"/>
-        	<xsl:with-param name="size" select="'+0'"/>
-       	</xsl:call-template>
-	<xsl:text> </xsl:text>
-	<xsl:apply-templates select="*[3]">
-	 <xsl:with-param name="current_indent" select="$current_indent"/> 
-	</xsl:apply-templates>
-	</xsl:when>
-	<xsl:otherwise>
-         <xsl:apply-templates mode="inline" select="."/>
-	</xsl:otherwise>
-	</xsl:choose>
-</xsl:template>
-
-<xsl:template match="m:integers">
-	<xsl:call-template name="mksymbol">
-        	<xsl:with-param name="symbol" select="$integers"/>
-        	<xsl:with-param name="color" select="'blue'"/>
-        	<xsl:with-param name="size" select="'+0'"/>
-       	</xsl:call-template>
-</xsl:template>
-
-<xsl:template match="m:naturalnumbers">
-	<xsl:call-template name="mksymbol">
-        	<xsl:with-param name="symbol" select="$naturalnumbers"/>
-        	<xsl:with-param name="size" select="'+0'"/>
-       	</xsl:call-template>
-</xsl:template>
-
-<xsl:template match="m:apply[m:implies]">
-    <xsl:param name="current_indent" select="0"/>
-	<xsl:variable name="charlength">
-	 <xsl:apply-templates select="m:implies" mode="charcount"/>
-	</xsl:variable>
-	<xsl:choose>
-	<xsl:when test="$charlength > $framewidth">
-			<xsl:text>implies</xsl:text>
-	<xsl:text>(</xsl:text>
-	<xsl:apply-templates select="*[2]">
-	 <xsl:with-param name="current_indent" select="$current_indent"/> 
-	</xsl:apply-templates>
-	<br/>
-	<xsl:call-template name="make_indent">
- 	 <xsl:with-param name="current_indent" select="$current_indent"/> 
-        </xsl:call-template>
-	<xsl:call-template name="mksymbol">
-        	<xsl:with-param name="symbol" select="$implies"/>
-        	<xsl:with-param name="color" select="'blue'"/>
-        	<xsl:with-param name="size" select="'+0'"/>
-       	</xsl:call-template>
-	<xsl:text> </xsl:text>
-	<xsl:apply-templates select="*[3]">
-	 <xsl:with-param name="current_indent" select="$current_indent"/> 
-	</xsl:apply-templates>
-	<xsl:text>)</xsl:text>
-	</xsl:when>
-	<xsl:otherwise>
-         <xsl:apply-templates mode="inline" select="."/>
-	</xsl:otherwise>
-	</xsl:choose>
-</xsl:template>
-
-<xsl:template  match="m:apply[m:exists]">
-  <xsl:param name="current_indent" select="0"/>
-	<xsl:variable name="charlength">
-	 <xsl:apply-templates select="m:implies" mode="charcount"/>
-	</xsl:variable>
-	<xsl:choose>
-	<xsl:when test="$charlength > $framewidth">
-	<xsl:call-template name="mksymbol">
-		<xsl:with-param name="symbol" select="$NUPRLexists"/>
-        	<xsl:with-param name="color" select="'blue'"/>
-		<xsl:with-param name="size" select="'+0'"/>
-	</xsl:call-template>
-	<xsl:apply-templates select="m:bvar/m:ci"/>
-     	<xsl:text>:</xsl:text>
-     	<!--<xsl:if test="count(m:condition/m:apply/*[3]) > 1">
-     		<xsl:text>(</xsl:text>
-     	</xsl:if>-->
-     	<xsl:apply-templates select="m:condition/m:apply/*[3]">
-	 <xsl:with-param name="current_indent" select="$current_indent"/> 
-	</xsl:apply-templates>
-     	<!--<xsl:if test="count(m:bvar/m:type/m:apply/*[3]) > 1">
-     		<xsl:text>)</xsl:text>
-     	</xsl:if>-->
-	<br/>
-	<xsl:call-template name="make_indent">
- 	 <xsl:with-param name="current_indent" select="$current_indent"/> 
-        </xsl:call-template>
-     	<xsl:text>.</xsl:text>
-     	<xsl:apply-templates select="*[position()=4]">
-	 <xsl:with-param name="current_indent" select="$current_indent"/> 
-	</xsl:apply-templates>
-	</xsl:when>
-	<xsl:otherwise>
-         <xsl:apply-templates mode="inline" select="."/>
-	</xsl:otherwise>
-	</xsl:choose>
-</xsl:template>
-
-<!--
-<xsl:template match="m:apply/m:ci">
-	<xsl:apply-templates/>
-	<xsl:text>(</xsl:text>
-	<xsl:for-each select="*[position()>1 and position()!=last()]">
-		<xsl:apply-templates/>
-		<xsl:text>, </xsl:text>
-	</xsl:for-each>
-	<xsl:apply-templates select="*[position()=last()]"/>
-	<xsl:text>)</xsl:text>
-</xsl:template>
--->
-<!-- enter this mode selecting the first child --> 
-
-<xsl:template match="m:ci|m:csymbol|m:implies|m:exists|m:interval|m:in" 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                                                               -->
-<!--***********************************************************************-->
-
-<!-- Rule -->
-
-<xsl:template match="Rule">
-<xsl:param name="current_indent" select="0"/>
-    
-    <xsl:variable name="char">
-     <xsl:value-of select="m:apply"/>
-    </xsl:variable>
-    <xsl:variable name="length" select="string-length($char)"/>
-    
-<p>
-<xsl:call-template name="make_indent">
- 	<xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:call-template>
-<FONT color="red">Rule: </FONT>
-<xsl:choose>
-	<xsl:when test="m:ci">
-		<FONT color="red">
-		<xsl:apply-templates>
-                 <xsl:with-param name="current_indent" select="$current_indent"/>
-		</xsl:apply-templates>
-		</FONT>
-	</xsl:when>
-	<xsl:otherwise>
-		<xsl:choose>
-		<xsl:when test="$length > $framewidth">
-		<br/>
-		<xsl:call-template name="make_indent">
- 	         <xsl:with-param name="current_indent" select="$current_indent"/> 
-                </xsl:call-template>
-		<xsl:variable name="char_rule">
-		 <xsl:value-of select="m:apply/*[1]"/>
-		</xsl:variable>
-		<xsl:variable name="length_rule" select="string-length($char_rule)"/>
-		<FONT>
-	         <xsl:apply-templates select="m:apply/*[1]">
- 	          <xsl:with-param name="current_indent" select="$current_indent"/>
-		 </xsl:apply-templates>
-		 <xsl:if test="count(m:apply/*)>2">
-		 <br/>
-		 <xsl:call-template name="make_indent">
- 	          <xsl:with-param name="current_indent" select="$current_indent + $length_rule"/> 
-                 </xsl:call-template>
-		 </xsl:if>
-		 <FONT color="red">
-		  <xsl:text> ( </xsl:text>
-		 </FONT>
-		</FONT>
-		<xsl:for-each select="m:apply/*[position()!=1]">
-		<xsl:if test="position()!=1">
-		<xsl:call-template name="make_indent">
- 	         <xsl:with-param name="current_indent" select="$current_indent + $length_rule"/> 
-                </xsl:call-template>
-		</xsl:if>
-		<xsl:choose>
-			<xsl:when test="*[1]='level-exp'">
-				<xsl:text>level-exp(</xsl:text>
-				<xsl:apply-templates select="*[2]">
-				 <xsl:with-param name="current_indent" select="$current_indent"/>
-				</xsl:apply-templates>
-				<xsl:text>)</xsl:text>
-			</xsl:when>
-			<xsl:when test="m:apply">
-				<xsl:apply-templates select=".">
- 	                         <xsl:with-param name="current_indent" select="$current_indent"/>
-				</xsl:apply-templates>
-			</xsl:when>
-			<xsl:otherwise>
-			 <xsl:apply-templates>
-		          <xsl:with-param name="current_indent" select="$current_indent"/>
-		         </xsl:apply-templates>
-			</xsl:otherwise>
-		</xsl:choose>
-		<xsl:if test="position()!=last()">
-			<xsl:text>, </xsl:text>
-			<br/>
-		</xsl:if>
-		</xsl:for-each>
-		<FONT color="red">
-		<xsl:text> )</xsl:text>
-		</FONT>
-
-		</xsl:when>
-		<xsl:otherwise>
-		<FONT>
-		<xsl:apply-templates select="m:apply/*[1]">
-		 <xsl:with-param name="current_indent" select="$current_indent"/>
-		</xsl:apply-templates>
-
-		<FONT color="red">
-		<xsl:text> ( </xsl:text>
-		</FONT>
-		</FONT>
-		<xsl:for-each select="m:apply/*[position()!=1]">
-		<xsl:choose>
-			<xsl:when test="*[1]='level-exp'">
-				<xsl:text>level-exp(</xsl:text>
-				<xsl:apply-templates select="*[2]">
-				 <xsl:with-param name="current_indent" select="$current_indent"/>
-				</xsl:apply-templates>
-                                <xsl:text>)</xsl:text>
-			</xsl:when>
-			<xsl:when test="m:apply">
-				<xsl:apply-templates select=".">
-				 <xsl:with-param name="current_indent" select="$current_indent"/>
-				</xsl:apply-templates>
-
-			</xsl:when>
-			<xsl:otherwise>
-				<xsl:apply-templates>
-				 <xsl:with-param name="current_indent" select="$current_indent"/>
-				</xsl:apply-templates>
-			</xsl:otherwise>
-		</xsl:choose>
-		<xsl:if test="position()!=last()">
-			<xsl:text>, </xsl:text>
-		</xsl:if>
-		</xsl:for-each>
-		<FONT color="red">
-		<xsl:text> )</xsl:text>
-		</FONT>
-		</xsl:otherwise>
-		</xsl:choose>
-	</xsl:otherwise>
-</xsl:choose>
-</p>
-</xsl:template>
-
-<!-- Sequent -->
-
-<xsl:template match="Sequent">
-<xsl:param name="current_indent" select="0"/>
-<xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/> 
-</xsl:call-template>
-<FONT color="red">Sequent <xsl:value-of select="@id"/></FONT>
-<br/>
-<br/>
-<xsl:for-each select="Decl">
-	<xsl:variable name="num" select="position()"/>
-	<xsl:call-template name="make_indent">
-         <xsl:with-param name="current_indent" select="$current_indent"/> 
-        </xsl:call-template>
-	<xsl:value-of select="$num"/>
-	<xsl:text>) </xsl:text>
-		<xsl:if test="@name">
-			<FONT color="green">
-			<xsl:value-of select="@name"/>
-			<xsl:text>:</xsl:text>
-			</FONT>
-		</xsl:if>
-		
-		<xsl:apply-templates>
-	 	 <xsl:with-param name="current_indent" select="$current_indent + 10"/>
-		</xsl:apply-templates>
-	<!--<xsl:choose>
-		<xsl:when test="m:apply">
-			<xsl:apply-templates select=".">
-			 <xsl:with-param name="current_indent" select="$current_indent"/>
-			</xsl:apply-templates>
-		</xsl:when>
-		<xsl:otherwise>
-			<xsl:apply-templates>
-			 <xsl:with-param name="current_indent" select="$current_indent"/>
-			</xsl:apply-templates>
-		</xsl:otherwise>
-	</xsl:choose>-->
-<br/>
- </xsl:for-each>
- <xsl:call-template name="make_indent">
-  <xsl:with-param name="current_indent" select="$current_indent"/> 
- </xsl:call-template>
-
- <FONT color="red" size="+1">|- </FONT>
- <br/>
- <xsl:call-template name="make_indent">
-  <xsl:with-param name="current_indent" select="$current_indent"/> 
- </xsl:call-template>
- <xsl:apply-templates select="Goal/*">
-  <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:apply-templates>
-</xsl:template>
-
-<!-- NODE -->
-
-<xsl:template match="Node">
- <xsl:param name="current_indent" select="0"/>
-
-       <xsl:variable name="nonce" select="generate-id()"/>
-       <xsl:variable name="freshid2" select="concat('b',$nonce)"/>
-       <xsl:variable name="freshid3" select="concat('c',$nonce)"/>
-       <xsl:variable name="freshid4" select="concat('d',$nonce)"/>
-       <xsl:variable name="freshid5" select="concat('e',$nonce)"/>
-       <br/>
-       <xsl:apply-templates select="Sequent">
-        <xsl:with-param name="current_indent" select="$current_indent"/>
-       </xsl:apply-templates>
-       <xsl:choose>
-        <xsl:when test="Rule">
-         <xsl:apply-templates select="Rule">
-          <xsl:with-param name="current_indent" select="$current_indent"/>
-         </xsl:apply-templates>
-        </xsl:when>
-        <xsl:when test="TacticInstance">
-         <br/>
-         <br/>
-	 <span>
-	  <xsl:call-template name="make_indent">
-           <xsl:with-param name="current_indent" select="$current_indent"/> 
-          </xsl:call-template>
-          <xsl:text>By </xsl:text>
-          <xsl:apply-templates select="TacticInstance/@name"/>
-          <a style="text-decoration:underline ; color:green" href="{TacticInstance/@uri}">Tactic Details</a>
-          <xsl:if test="$explode_tactics">
-	   <span ID="{$freshid4}">
-            <a style="text-decoration:underline ; color:green" href="" onClick="Hide(document.getElementById('{$freshid4}'));Show(document.getElementById('{$freshid5}'));return (0==1);">Details</a>
-           </span>
-          </xsl:if>
-         </span>
-         <xsl:if test="$explode_tactics">
-          <div ID="{$freshid5}">
-	   <xsl:call-template name="make_indent">
-            <xsl:with-param name="current_indent" select="$current_indent"/> 
-           </xsl:call-template>
-           <a style="text-decoration:underline ; color:red" href="" onClick="Show(document.getElementById('{$freshid4}'));Hide(document.getElementById('{$freshid5}'));return (0==1);">Hide details</a>
-	   <br/>
-	   <xsl:apply-templates select="TacticProof">
-	  	 <xsl:with-param name="current_indent" select="$current_indent + 5"/>
-	   </xsl:apply-templates>
-          </div>
-         </xsl:if>
-         <br/><br/>
-        </xsl:when>
-       </xsl:choose>
-        <xsl:if test="count(Node)!=0">
-            <xsl:choose> 
-	    <xsl:when test="count(Node)=1">
-	    <span ID="{$freshid2}">
-	     <xsl:call-template name="make_indent">
-              <xsl:with-param name="current_indent" select="$current_indent"/> 
-             </xsl:call-template>
-             <a style="text-decoration:underline ; color:green" href="" onClick="Hide(document.getElementById('{$freshid2}'));Show(document.getElementById('{$freshid3}'));return (0==1);">Subgoal</a>
-	     <br/>
-            </span>
-	    </xsl:when>
-	    <xsl:otherwise>
-	    <span ID="{$freshid2}">
-	     <xsl:call-template name="make_indent">
-              <xsl:with-param name="current_indent" select="$current_indent"/> 
-             </xsl:call-template>
-             <a style="text-decoration:underline ; color:green" href="" onClick="Hide(document.getElementById('{$freshid2}'));Show(document.getElementById('{$freshid3}'));return (0==1);">Subgoals</a>
-	     <br/>
-            </span>
-	    </xsl:otherwise>
-	    </xsl:choose>
-            <div ID="{$freshid3}">
-	     <xsl:call-template name="make_indent">
-              <xsl:with-param name="current_indent" select="$current_indent"/> 
-             </xsl:call-template>
-             <a style="text-decoration:underline ; color:red" href="" onClick="Show(document.getElementById('{$freshid2}'));Hide(document.getElementById('{$freshid3}'));return (0==1);">Back</a>
-	     <br/>
-	     <xsl:apply-templates select="Node">
-	     	<xsl:with-param name="current_indent" select="$current_indent + 5"/>
-	     </xsl:apply-templates>
-            </div>
-	  <script>
-           document.to_be_deleted.push('<xsl:value-of select="$freshid3"/>');
-	  </script>
-	  </xsl:if>
-</xsl:template>
-
-<!-- NuPRLDefinition -->
-
-<xsl:template match="NuPrlDefinition">
- <xsl:apply-templates select="*[1]"/>
- <xsl:text> := </xsl:text>
- <xsl:apply-templates select="*[2]"/>
-</xsl:template>
-
-<!-- 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/Node">
-        <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 =<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>
-</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:for-each select="Decl|Def|Hidden">
-       <xsl:choose>
-        <xsl:when test="name(.)='Decl'">
-         <xsl:choose>
-          <xsl:when test="@name">
-           <xsl:value-of select="@name"/>
-          </xsl:when>
-          <xsl:otherwise>
-           <xsl:text>_</xsl:text>
-          </xsl:otherwise>
-         </xsl:choose>
-         <xsl:text> : </xsl:text>
-         <xsl:apply-templates select="./*[1]">
-          <xsl:with-param name="current_indent" select="$current_indent"/>
-         </xsl:apply-templates>
-        </xsl:when>
-        <xsl:when test="name(.)='Def'">
-         <xsl:choose>
-          <xsl:when test="@name">
-           <xsl:value-of select="@name"/>
-          </xsl:when>
-          <xsl:otherwise>
-           <xsl:text>_</xsl:text>
-          </xsl:otherwise>
-         </xsl:choose>
-         <xsl:text> := </xsl:text>
-         <xsl:apply-templates select="./*[1]">
-          <xsl:with-param name="current_indent" select="$current_indent"/>
-         </xsl:apply-templates>
-        </xsl:when>
-        <xsl:otherwise>
-         <xsl:text> _ :? _ </xsl:text>
-        </xsl:otherwise>
-       </xsl:choose>
-      </xsl:for-each>
-      |- <xsl:value-of select="./@no"/> : 
-      <xsl:apply-templates select="./Goal/*[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 + 2*string-length(./@name) + 5"/>
-         </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>
-<xsl:if test="body">
-<br/>
-BODY = <xsl:apply-templates select="body/*[1]">
-          <xsl:with-param name="current_indent" select="$current_indent + 7"/>
-       </xsl:apply-templates>
-</xsl:if>
-</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>