--- /dev/null
+<?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:variable name="PIPPOUNICODEvsSYMBOL" 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="$PIPPOUNICODEvsSYMBOL = 'symbol'">"</xsl:when>
+ <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'unicode'">∀</xsl:when>
+ <xsl:otherwise>???</xsl:otherwise>
+ </xsl:choose>
+ </xsl:variable>
+<!--lambda-->
+ <xsl:variable name="lambda">
+ <xsl:choose>
+ <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'symbol'">l</xsl:when>
+ <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'unicode'">λ</xsl:when>
+ <xsl:otherwise>???</xsl:otherwise>
+ </xsl:choose>
+ </xsl:variable>
+<!--prod-->
+ <xsl:variable name="prod">
+ <xsl:choose>
+ <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'symbol'">Õ</xsl:when>
+ <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'unicode'">Π</xsl:when>
+ <xsl:otherwise>???</xsl:otherwise>
+ </xsl:choose>
+ </xsl:variable>
+<!--arrow-->
+ <xsl:variable name="arrow">
+ <xsl:choose>
+ <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'symbol'">®</xsl:when>
+ <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'unicode'">→</xsl:when>
+ <xsl:otherwise>???</xsl:otherwise>
+ </xsl:choose>
+ </xsl:variable>
+<!--RightArrow-->
+ <xsl:variable name="RightArrow">
+ <xsl:choose>
+ <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'symbol'">Þ</xsl:when>
+ <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'unicode'">⇒</xsl:when>
+ <xsl:otherwise>???</xsl:otherwise>
+ </xsl:choose>
+ </xsl:variable>
+<!--product-->
+ <xsl:variable name="product">
+ <xsl:choose>
+ <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'symbol'">S</xsl:when>
+ <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'unicode'">Σ</xsl:when>
+ <xsl:otherwise>???</xsl:otherwise>
+ </xsl:choose>
+ </xsl:variable>
+<!--member-->
+ <xsl:variable name="member">
+ <xsl:choose>
+ <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'symbol'">Î</xsl:when>
+ <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'unicode'">∈</xsl:when>
+ <xsl:otherwise>???</xsl:otherwise>
+ </xsl:choose>
+ </xsl:variable>
+<!--member-->
+ <xsl:variable name="intersection">
+ <xsl:choose>
+ <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'symbol'">Ç</xsl:when>
+ <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'unicode'">∩</xsl:when>
+ <xsl:otherwise>???</xsl:otherwise>
+ </xsl:choose>
+ </xsl:variable>
+<!--integers-->
+ <xsl:variable name="integers">
+ <xsl:choose>
+ <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'symbol'">I</xsl:when>
+ <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'unicode'">Ι</xsl:when>
+ <xsl:otherwise>???</xsl:otherwise>
+ </xsl:choose>
+ </xsl:variable>
+<!--naturalnumbers-->
+ <xsl:variable name="naturalnumbers">
+ <xsl:choose>
+ <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'symbol'">N</xsl:when>
+ <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'unicode'">Ν</xsl:when>
+ <xsl:otherwise>???</xsl:otherwise>
+ </xsl:choose>
+ </xsl:variable>
+<!--implies-->
+ <xsl:variable name="implies">
+ <xsl:choose>
+ <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'symbol'">î</xsl:when>
+ <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'unicode'">⇒</xsl:when>
+ <xsl:otherwise>???</xsl:otherwise>
+ </xsl:choose>
+ </xsl:variable>
+<!--exists-->
+ <xsl:variable name="exists">
+ <xsl:choose>
+ <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'symbol'">$</xsl:when>
+ <xsl:when test="$PIPPOUNICODEvsSYMBOL = 'unicode'">∃</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="$PIPPOUNICODEvsSYMBOL = '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<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> </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=""">
+ <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><</xsl:text>
+ </FONT>
+ <xsl:apply-templates select="*[2]"/>
+ <xsl:text>, </xsl:text>
+ <xsl:apply-templates select="*[3]"/>
+ <FONT color="blue" size="+1">
+ <xsl:text>></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> </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(*) > 2">
+ <xsl:text>(</xsl:text>
+ <xsl:for-each select="*[position() > 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> </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><</xsl:text>
+ <xsl:apply-templates mode="inline" select="*[position()=2]"/>
+ <xsl:text>> </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"> proves </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 </FONT>
+ <xsl:apply-templates select="*[2]"/>
+ <FONT color="red"> we get</FONT>
+ (
+ <xsl:apply-templates select="*[3]"/>
+ ) 
+ <xsl:apply-templates mode="inline" select="*[4]"/>
+ <FONT color="red"> and </FONT>
+ (
+ <xsl:apply-templates select="*[5]"/>
+ ) 
+ <xsl:apply-templates mode="inline" select="*[6]"/>
+ ;
+ <FONT color="red"> hence </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=""">
+ <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">
+ <!-- Π -->
+ <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><</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>></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(*) > 2">
+ <xsl:text>(</xsl:text>
+ <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="." 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><</xsl:text>
+ <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: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>  </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 </xsl:text>
+ <xsl:apply-templates select="m:bvar/m:ci"/>
+ <xsl:text> := </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 </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>
+  
+ </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 </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(' ');
+ } 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 </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>
+  
+ </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(' ');
+ } 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 </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> =</xsl:text>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:text>= </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> </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> </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 </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 </FONT>
+ <xsl:apply-templates mode="inline" select="*[3]"/>
+ <xsl:text> </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 </FONT>
+ <xsl:apply-templates mode="inline" select="*[4]"/>
+ <xsl:text> </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 </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 </FONT>
+ <xsl:apply-templates select="*[position()>2]"/>
+ </xsl:when>
+ <!-- by_induction -->
+ <xsl:when test="$name='by_induction'">
+ <FONT color="red">We prove </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 </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 </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>) </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> </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 </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]"/>
+ ) 
+ <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]"/>
+ ) 
+ <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 </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 </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 </FONT>
+ <xsl:text>(</xsl:text>
+ <xsl:value-of select="*[4]/m:bvar/m:ci"/>
+ <xsl:text>) </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 </FONT>
+ <xsl:text>(</xsl:text>
+ <xsl:value-of select="*[5]/m:bvar/m:ci"/>
+ <xsl:text>) </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 </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 </FONT>
+ <xsl:apply-templates select="*[3]"/>
+ <FONT color="red"> by cases:</FONT>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent"/>
+ </xsl:call-template>
+ Left: 
+ <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: 
+ <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 </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 </FONT>
+ <xsl:apply-templates mode="inline" select="*[3]"/>
+ :
+ <xsl:apply-templates mode="inline" select="*[4]"/>
+ <FONT color="red"> 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">
+ <!-- λ -->
+ <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="$exists"/>
+ <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="$exists"/>
+ <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) = """>
+ <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) = """>
+ <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"/>
+ <!-- CSC: extra_info in HTML to be rendered here -->
+ <xsl:for-each select="TacticInstance/extra_info">
+ <xsl:copy-of select="*|text()"/>
+ </xsl:for-each>
+ <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>
+
+<!-- DEFINITION -->
+
+<xsl:template match="Definition">
+<xsl:param name="current_indent" select="0"/>
+<p>
+DEFINITION <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != """><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) != """><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) != """><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) = "true"">
+ 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) != """><xsl:value-of select="../Params"/></xsl:if>)
+ [
+ <xsl:if test="string(../Param) != """>
+ <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>  </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>
projects / helm.git / blobdiff