3 <!-- Copyright (C) 2000, HELM Team -->
5 <!-- This file is part of HELM, an Hypertextual, Electronic -->
6 <!-- Library of Mathematics, developed at the Computer Science -->
7 <!-- Department, University of Bologna, Italy. -->
9 <!-- HELM is free software; you can redistribute it and/or -->
10 <!-- modify it under the terms of the GNU General Public License -->
11 <!-- as published by the Free Software Foundation; either version 2 -->
12 <!-- of the License, or (at your option) any later version. -->
14 <!-- HELM is distributed in the hope that it will be useful, -->
15 <!-- but WITHOUT ANY WARRANTY; without even the implied warranty of -->
16 <!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -->
17 <!-- GNU General Public License for more details. -->
19 <!-- You should have received a copy of the GNU General Public License -->
20 <!-- along with HELM; if not, write to the Free Software -->
21 <!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston, -->
22 <!-- MA 02111-1307, USA. -->
24 <!-- For details, see the HELM World-Wide-Web page, -->
25 <!-- http://cs.unibo.it/helm/. -->
27 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
28 xmlns:m="http://www.w3.org/1998/Math/MathML">
30 <!--***********************************************************************-->
31 <!-- From MathML content to HTML -->
32 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena, Guidi -->
33 <!--***********************************************************************-->
35 <xsl:param name="CICURI" select="''"/>
36 <xsl:param name="type" select="'standalone'"/>
37 <xsl:param name="UNICODEvsSYMBOL" select="'symbol'"/>
38 <xsl:param name="explode_tactics" select="false()"/>
40 <xsl:include href="nuprl_html_arith.xsl"/>
41 <xsl:include href="nuprl_html_basic.xsl"/>
43 <xsl:variable name="showcast" select="0"/>
45 <!--***********************************************************************-->
46 <!-- HTML Head and Body -->
47 <!--***********************************************************************-->
49 <!-- <xsl:output method="html" encoding="utf8"/> -->
51 <!-- document needs method="xml" and searches locally for the dtd if -->
52 <!-- doctype-system is specified (the dtd must exist locally for parsing). -->
53 <!-- For having output html must be media-type="html" and for having the -->
54 <!-- correct <br /> you must specify at least the remote dtd by means of -->
55 <!-- doctype-public -->
57 <!-- Commentd out by Zack, a try-fix for NuPRL stylesheets with OCaml UWOBO -->
62 media-type="text/html"
63 doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN" />
68 media-type="text/html"
69 doctype-public="-//W3C//DTD XHTML 1.0 Transitional//EN" />
71 <xsl:variable name="framewidth" select="55"/>
74 <xsl:variable name="forall">
76 <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">"</xsl:when>
77 <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">∀</xsl:when>
78 <xsl:otherwise>???</xsl:otherwise>
82 <xsl:variable name="lambda">
84 <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">l</xsl:when>
85 <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">λ</xsl:when>
86 <xsl:otherwise>???</xsl:otherwise>
90 <xsl:variable name="prod">
92 <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">Õ</xsl:when>
93 <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">Π</xsl:when>
94 <xsl:otherwise>???</xsl:otherwise>
98 <xsl:variable name="arrow">
100 <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">®</xsl:when>
101 <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">→</xsl:when>
102 <xsl:otherwise>???</xsl:otherwise>
106 <xsl:variable name="RightArrow">
108 <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">Þ</xsl:when>
109 <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">⇒</xsl:when>
110 <xsl:otherwise>???</xsl:otherwise>
114 <xsl:variable name="product">
116 <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">S</xsl:when>
117 <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">Σ</xsl:when>
118 <xsl:otherwise>???</xsl:otherwise>
122 <xsl:variable name="member">
124 <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">Î</xsl:when>
125 <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">∈</xsl:when>
126 <xsl:otherwise>???</xsl:otherwise>
130 <xsl:variable name="intersection">
132 <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">Ç</xsl:when>
133 <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">∩</xsl:when>
134 <xsl:otherwise>???</xsl:otherwise>
138 <xsl:variable name="integers">
140 <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">I</xsl:when>
141 <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">Ι</xsl:when>
142 <xsl:otherwise>???</xsl:otherwise>
145 <!--naturalnumbers-->
146 <xsl:variable name="naturalnumbers">
148 <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">N</xsl:when>
149 <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">Ν</xsl:when>
150 <xsl:otherwise>???</xsl:otherwise>
154 <xsl:variable name="implies">
156 <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">î</xsl:when>
157 <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">⇒</xsl:when>
158 <xsl:otherwise>???</xsl:otherwise>
162 <xsl:variable name="NUPRLexists">
164 <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">$</xsl:when>
165 <xsl:when test="$UNICODEvsSYMBOL = 'unicode'">∃</xsl:when>
166 <xsl:otherwise>???</xsl:otherwise>
172 <xsl:template name="mksymbol">
173 <xsl:param name="symbol" select="'???'"/>
174 <xsl:param name="color" select="'blue'"/>
175 <xsl:param name="size" select="''"/>
178 <xsl:when test="$UNICODEvsSYMBOL = 'symbol'">
179 <FONT FACE="symbol" SIZE="{$size}" COLOR="{$color}">
180 <xsl:value-of select="$symbol"/>
184 <FONT COLOR="{$color}">
185 <xsl:value-of select="$symbol"/>
191 <xsl:template match="/">
192 <xsl:param name="current_indent" select="0"/>
194 <xsl:when test="$type = 'standalone'">
197 <title> <xsl:value-of select="$CICURI"/> </title> <!-- FG -->
198 <style> A { text-decoration: none } </style>
200 <xsl:text disable-output-escaping="yes">
202 function Hide(which){
203 if (!document.getElementById)
205 which.style.display="none"
208 function Show(which){
209 if (!document.getElementById)
211 which.style.display=""
214 document.to_be_deleted = new Array();
219 <body bgcolor="white">
220 <xsl:attribute name="onLoad">
221 if(document.getElementById)
222 for(var i=0;i<document.to_be_deleted.length;i++)
223 Hide(document.getElementById(document.to_be_deleted[i]));
225 <xsl:apply-templates>
226 <xsl:with-param name="current_indent" select="0"/>
227 </xsl:apply-templates>
233 <xsl:apply-templates>
234 <xsl:with-param name="current_indent" select="0"/>
235 </xsl:apply-templates>
241 <!--***********************************************************************-->
243 <!--***********************************************************************-->
245 <xsl:template name="make_indent">
246 <xsl:param name="current_indent" select="0"/>
247 <xsl:if test="$current_indent > 0">
248 <xsl:text> </xsl:text>
249 <xsl:call-template name="make_indent">
250 <xsl:with-param name="current_indent" select="$current_indent - 1"/>
255 <!-- Syntactic Sugar -->
256 <xsl:template match="m:type">
257 <xsl:param name="current_indent" select="0"/>
258 <xsl:apply-templates>
259 <xsl:with-param name="current_indent"
260 select="$current_indent"/>
261 </xsl:apply-templates>
264 <xsl:template match="m:condition">
265 <xsl:param name="current_indent" select="0"/>
266 <xsl:apply-templates>
267 <xsl:with-param name="current_indent"
268 select="$current_indent"/>
269 </xsl:apply-templates>
272 <xsl:template match="m:math">
273 <xsl:param name="current_indent" select="0"/>
274 <xsl:apply-templates>
275 <xsl:with-param name="current_indent"
276 select="$current_indent"/>
277 </xsl:apply-templates>
282 <!--*********************************************************************-->
284 <!--*********************************************************************-->
287 <xsl:template mode="inline" match="m:ci">
289 <xsl:when test="boolean(@definitionURL)">
290 <a href="{@definitionURL}">
291 <xsl:apply-templates/>
295 <xsl:value-of select="."/>
302 <xsl:template match="m:apply[m:csymbol]" mode="inline">
303 <xsl:param name="current_indent" select="0"/>
304 <xsl:variable name="name">
305 <xsl:value-of select="m:csymbol"/>
307 <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
310 <!-- FUNCTION-DIP (PROD) -->
311 <xsl:when test="$name='prod'">
312 <xsl:call-template name="mksymbol">
313 <xsl:with-param name="symbol" select="$prod"/>
314 <xsl:with-param name="color" select="'blue'"/>
315 <xsl:with-param name="size" select="'+2'"/>
317 <xsl:apply-templates select="m:bvar/m:ci"/>
318 <xsl:if test="m:bvar/m:ci=""">
319 <xsl:text>""</xsl:text>
321 <xsl:text>:</xsl:text>
322 <!--<xsl:if test="m:bvar/m:type/*[*]">
323 <xsl:text>( </xsl:text>
325 <xsl:apply-templates select="m:bvar/m:type"/>
326 <!--<xsl:if test="m:bvar/m:type/*[*]">
327 <xsl:text>) </xsl:text>
329 <xsl:text>.</xsl:text>
330 <xsl:apply-templates select="*[position()=3]"/>
333 <!-- ARROW --> <!-- FUNCTION (IND) -->
334 <xsl:when test="$name='arrow'">
335 <xsl:text>(</xsl:text>
336 <xsl:apply-templates mode="inline" select="*[position()=2]"/>
337 <xsl:call-template name="mksymbol">
338 <xsl:with-param name="symbol" select="$arrow"/>
339 <xsl:with-param name="color" select="'blue'"/>
340 <xsl:with-param name="size" select="'+0'"/>
342 <xsl:apply-templates select="*[position()=3]"/>
343 <xsl:text>)</xsl:text>
348 <xsl:when test="$name='forall'">
349 <xsl:call-template name="mksymbol">
350 <xsl:with-param name="symbol" select="$forall"/>
351 <xsl:with-param name="color" select="'blue'"/>
352 <xsl:with-param name="size" select="'+2'"/>
354 <xsl:apply-templates select="m:bvar/m:ci"/>
355 <xsl:text>:</xsl:text>
356 <!--<xsl:if test="count(m:bvar/m:type/m:apply/*) > 1">
357 <xsl:text>(</xsl:text>
359 <xsl:apply-templates select="m:bvar/m:type"/>
360 <!--<xsl:if test="count(m:bvar/m:type/m:apply/*) > 1">
361 <xsl:text>)</xsl:text>
363 <xsl:text>.</xsl:text>
364 <xsl:apply-templates select="*[position()=3]"/>
369 <xsl:when test="$name='product'">
370 <xsl:call-template name="mksymbol">
371 <xsl:with-param name="symbol" select="$product"/>
372 <xsl:with-param name="color" select="'blue'"/>
373 <xsl:with-param name="size" select="'+2'"/>
375 <xsl:apply-templates select="m:bvar/m:ci"/>
376 <xsl:text>:</xsl:text>
377 <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
378 <xsl:text>.</xsl:text>
379 <xsl:apply-templates select="*[position()=3]"/>
383 <xsl:when test="$name='product_ind'">
385 <xsl:text>( </xsl:text>
387 <xsl:apply-templates mode="inline" select="m:type"/>
388 <FONT color="blue" size="+2">
389 <xsl:text>x</xsl:text>
391 <xsl:apply-templates mode="inline" select="*[position()=3]"/>
393 <xsl:text> )</xsl:text>
399 <xsl:when test="$name='pair'">
400 <FONT color="blue" size="+1">
401 <xsl:text><</xsl:text>
403 <xsl:apply-templates select="*[2]"/>
404 <xsl:text>, </xsl:text>
405 <xsl:apply-templates select="*[3]"/>
406 <FONT color="blue" size="+1">
407 <xsl:text>></xsl:text>
412 <xsl:when test="$name='union'">
413 <xsl:apply-templates select="*[2]"/>
414 <FONT color="blue" size="+2">
415 <xsl:text>+</xsl:text>
417 <xsl:apply-templates select="*[3]"/>
421 <xsl:when test="$name='inl'">
423 <xsl:text>inl (</xsl:text>
425 <xsl:apply-templates select="*[2]"/>
427 <xsl:text> )</xsl:text>
432 <xsl:when test="$name='inr'">
433 <FONT color="blue" size="+1">
434 <xsl:text>inr (</xsl:text>
436 <xsl:apply-templates select="*[2]"/>
437 <FONT color="blue" size="+1">
438 <xsl:text> )</xsl:text>
443 <xsl:when test="$name='equal'">
444 <xsl:apply-templates select="*[position()=3]"/>
445 <FONT color="blue" size="+1">
446 <xsl:text> = </xsl:text>
448 <xsl:apply-templates select="*[position()=4]"/>
449 <xsl:text> </xsl:text>
450 <xsl:call-template name="mksymbol">
451 <xsl:with-param name="symbol" select="$member"/>
452 <xsl:with-param name="color" select="'blue'"/>
453 <xsl:with-param name="size" select="'+0'"/>
455 <xsl:text> </xsl:text>
456 <xsl:apply-templates select="*[position()=2]">
457 <xsl:with-param name="current_indent" select="$current_indent"/>
458 </xsl:apply-templates>
462 <xsl:when test="$name='cons'">
463 <xsl:apply-templates select="*[2]"/>
465 <xsl:text>::</xsl:text>
467 <xsl:apply-templates select="*[3]"/>
472 <xsl:when test="$name='rec'">
474 <xsl:text>rectype</xsl:text>
476 <xsl:apply-templates select="*[2]"/>
478 <xsl:text>=</xsl:text>
480 <xsl:apply-templates select="*[3]"/>
486 <xsl:when test="$name='t_set'">
488 <xsl:text>{</xsl:text>
491 <xsl:when test="m:bvar/m:ci">
492 <xsl:apply-templates select="m:bvar/m:ci"/>
494 <xsl:text>:</xsl:text>
496 <xsl:apply-templates select="m:bvar/m:type"/>
499 <xsl:apply-templates select="m:bvar/m:type"/>
503 <xsl:text>|</xsl:text>
505 <xsl:apply-templates select="*[3]"/>
507 <xsl:text>}</xsl:text>
514 <xsl:when test="$name='isect'">
515 <xsl:call-template name="mksymbol">
516 <xsl:with-param name="symbol" select="$intersection"/>
517 <xsl:with-param name="color" select="'blue'"/>
518 <xsl:with-param name="size" select="'+0'"/>
520 <xsl:apply-templates select="m:bvar/m:ci"/>
522 <xsl:text>:</xsl:text>
524 <xsl:apply-templates select="m:bvar/m:type"/>
526 <xsl:text>.</xsl:text>
528 <xsl:apply-templates select="*[3]"/>
533 <xsl:when test="$name='quotient'">
534 <xsl:apply-templates select="m:bvar[1]"/>
535 <xsl:text>,</xsl:text>
536 <xsl:apply-templates select="m:bvar[2]"/>
538 <xsl:text>:</xsl:text>
540 <xsl:apply-templates select="*[2]"/>
542 <xsl:text>//</xsl:text>
544 <xsl:apply-templates select="*[5]"/>
548 <xsl:when test="$name='so_lambda'">
549 <xsl:call-template name="mksymbol">
550 <xsl:with-param name="symbol" select="$lambda"/>
551 <xsl:with-param name="color" select="'red'"/>
552 <xsl:with-param name="size" select="'+2'"/>
554 <xsl:apply-templates select="m:apply[1]/*[2]"/>
555 <xsl:text>.</xsl:text>
556 <xsl:apply-templates select="*[3]"/>
562 <xsl:when test="$name='so_apply'">
563 <xsl:text>(</xsl:text>
564 <xsl:apply-templates select="*[position()=2]"/>
565 <xsl:for-each select="*[position()>2]">
566 <xsl:text> </xsl:text>
567 <xsl:apply-templates mode="inline" select="."/>
569 <xsl:text>)</xsl:text>
572 <xsl:when test="$name='app'">
573 <!-- NuPRL rendering -->
574 <xsl:apply-templates mode="inline" select="*[position()=2]"/>
575 <xsl:if test="count(*) > 2">
576 <xsl:text>(</xsl:text>
577 <xsl:for-each select="*[position() > 2]">
578 <xsl:apply-templates select="." mode="inline"/>
579 <xsl:if test="not(position() = last())">
580 <xsl:text>,</xsl:text>
583 <xsl:text>)</xsl:text>
586 <xsl:text>(</xsl:text>
587 <xsl:apply-templates mode="inline" select="*[position()=2]"/>
588 <xsl:for-each select="*[position()>2]">
589 <xsl:text> </xsl:text>
590 <xsl:apply-templates mode="inline" select="."/>
592 <xsl:text>)</xsl:text>
596 <xsl:when test="$name='cast'">
597 <xsl:text>(</xsl:text>
598 <xsl:apply-templates mode="inline" select="*[position()=2]"/>
599 <xsl:text>:></xsl:text>
600 <xsl:apply-templates mode="inline" select="*[position()=3]"/>
601 <xsl:text>)</xsl:text>
603 <xsl:when test="$name='Prop'">
604 <FONT color="violet">Prop</FONT>
606 <xsl:when test="$name='Set'">
607 <FONT color="violet">Set</FONT>
609 <xsl:when test="$name='Type'">
610 <FONT color="violet">Type</FONT>
614 <xsl:when test="$name='mutcase'">
615 <xsl:text><</xsl:text>
616 <xsl:apply-templates mode="inline" select="*[position()=2]"/>
617 <xsl:text>> </xsl:text>
618 <FONT color="red">CASE </FONT>
619 <xsl:apply-templates mode="inline" select="*[position()=3]"/>
620 <FONT color="red"> OF </FONT>
621 <xsl:for-each select="m:piecewise/m:piece">
622 <!--<xsl:for-each select="*[position() mod 2 = 0 and position()>3]">-->
624 <xsl:when test="not(position() = 1)">
625 <xsl:text> | </xsl:text>
628 <xsl:apply-templates mode="inline" select="./*[2]"/>
629 <xsl:call-template name="mksymbol">
630 <xsl:with-param name="symbol" select="$RightArrow"/>
631 <xsl:with-param name="color" select="'green'"/>
632 <xsl:with-param name="size" select="'+0'"/>
634 <xsl:apply-templates mode="inline"
640 <xsl:when test="$name='fix'">
641 <FONT color="red">FIX</FONT>
642 <xsl:value-of select="m:ci"/>
643 <xsl:text>{</xsl:text>
644 <xsl:for-each select="m:bvar">
645 <xsl:value-of select="m:ci"/>
646 <xsl:text>:</xsl:text>
647 <xsl:apply-templates mode="inline" select="m:type"/>
648 <xsl:text>:=</xsl:text>
649 <xsl:apply-templates mode="inline"
650 select="following-sibling::*[position() = 1]"/>
652 <xsl:when test="position()=last()">
653 <xsl:text>}</xsl:text>
656 <xsl:text>;</xsl:text>
663 <xsl:when test="$name='cofix'">
664 <xsl:text>COFIX</xsl:text>
665 <xsl:value-of select="m:ci"/>
666 <xsl:text>{</xsl:text>
667 <xsl:for-each select="m:bvar">
668 <xsl:value-of select="m:ci"/>
669 <xsl:text>:</xsl:text>
670 <xsl:apply-templates mode="inline" select="m:type"/>
671 <xsl:text>:=</xsl:text>
672 <xsl:apply-templates mode="inline"
673 select="following-sibling::*[position() = 1]"/>
675 <xsl:when test="position()=last()">
676 <xsl:text>}</xsl:text>
679 <xsl:text>;</xsl:text>
686 <xsl:when test="$name='proof' or $name='side_proof'">
687 <xsl:apply-templates mode="inline" select="*[position()=2]"/>
688 <FONT color="red"> proves </FONT>
689 <xsl:apply-templates mode="inline" select="*[position()=3]"/>
691 <xsl:when test="$name='letin1'">
692 <xsl:text>letin1 (inline error)</xsl:text>
695 <xsl:when test="$name='false_ind'">
696 <xsl:apply-templates mode="inline" select="*[3]"/>
697 <FONT color="red">Contradiction.</FONT>
700 <xsl:when test="$name='and_ind'">
701 <FONT color="red">From </FONT>
702 <xsl:apply-templates select="*[2]"/>
703 <FONT color="red"> we get</FONT>
705 <xsl:apply-templates select="*[3]"/>
707 <xsl:apply-templates mode="inline" select="*[4]"/>
708 <FONT color="red"> and </FONT>
710 <xsl:apply-templates select="*[5]"/>
712 <xsl:apply-templates mode="inline" select="*[6]"/>
714 <FONT color="red"> hence </FONT>
715 <xsl:apply-templates mode="inline" select="*[7]"/>
720 <xsl:template mode="inline" match="m:lambda">
721 <xsl:call-template name="mksymbol">
722 <xsl:with-param name="symbol" select="$lambda"/>
723 <xsl:with-param name="color" select="'red'"/>
724 <xsl:with-param name="size" select="'+2'"/>
727 <!-- IN NuPrl non e' specificato il tipo -->
728 <xsl:apply-templates select="m:bvar/m:ci"/>
729 <xsl:if test="m:bvar[m:mtype]">
730 <xsl:text>:</xsl:text>
731 <xsl:apply-templates mode="inline" select="m:bvar/m:type"/>
733 <xsl:text>.</xsl:text>
734 <xsl:apply-templates mode="inline" select="*[position()=2]"/>
737 <!--*********************************************************************-->
739 <!--*********************************************************************-->
741 <xsl:template match="m:apply[m:csymbol]">
742 <xsl:param name="current_indent" select="0"/>
743 <xsl:param name="width" select="$framewidth"/>
744 <xsl:variable name="name">
745 <xsl:value-of select="m:csymbol"/>
747 <xsl:variable name="charlength">
748 <xsl:apply-templates select="m:csymbol" mode="charcount"/>
750 <xsl:variable name="uri">
751 <xsl:value-of select="*[1]/@definitionURL"/>
757 <!-- FUNCTION-DIP (PROD) -->
758 <xsl:when test="$name='prod'">
760 <xsl:when test="$charlength > $framewidth">
761 <xsl:call-template name="mksymbol">
762 <xsl:with-param name="symbol" select="$prod"/>
763 <xsl:with-param name="color" select="'blue'"/>
764 <xsl:with-param name="size" select="'+2'"/>
766 <xsl:apply-templates select="m:bvar/m:ci">
767 <xsl:with-param name="current_indent" select="$current_indent"/>
768 </xsl:apply-templates>
769 <xsl:if test="m:bvar/m:ci=""">
770 <xsl:text>""</xsl:text>
772 <xsl:text>:</xsl:text>
773 <!--<xsl:if test="m:bvar/m:type/*[*]">
774 <xsl:text>( </xsl:text>
776 <xsl:apply-templates select="m:bvar/m:type">
777 <xsl:with-param name="current_indent"
778 select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
779 </xsl:apply-templates>
780 <!--<xsl:if test="m:bvar/m:type/*[*]">
781 <xsl:text>) </xsl:text>
784 <xsl:call-template name="make_indent">
785 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
787 <xsl:text>.</xsl:text>
788 <xsl:apply-templates select="*[position()=3]">
789 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
790 </xsl:apply-templates>
793 <xsl:apply-templates mode="inline" select="."/>
798 <!-- ARROW --> <!-- FUNCTION IND -->
799 <xsl:when test="$name='arrow'">
801 <xsl:when test="$charlength > $framewidth">
802 <xsl:text>arrow</xsl:text>
803 <xsl:text>(</xsl:text>
804 <xsl:apply-templates select="*[position()=2]">
805 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
806 </xsl:apply-templates>
808 <xsl:call-template name="make_indent">
809 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
812 <xsl:text> </xsl:text>
813 <xsl:call-template name="mksymbol">
814 <xsl:with-param name="symbol" select="$arrow"/>
815 <xsl:with-param name="color" select="'blue'"/>
816 <xsl:with-param name="size" select="'+0'"/>
818 <xsl:apply-templates select="*[position()=3]">
819 <xsl:with-param name="current_indent" select="$current_indent + 5"/>
820 </xsl:apply-templates>
821 <xsl:text>)</xsl:text>
824 <xsl:apply-templates mode="inline" select="."/>
830 <xsl:when test="$name='type_of'">
831 <xsl:value-of select="*[2]"/>
832 <xsl:text>:</xsl:text>
833 <xsl:if test="count(*[3]/*) > 1">
834 <xsl:text>(</xsl:text>
836 <xsl:apply-templates select="*[3]"/>
837 <xsl:if test="count(*[3]/*) > 1">
838 <xsl:text>)</xsl:text>
843 <xsl:when test="$name='Ax'">
845 <xsl:text>Ax</xsl:text>
850 <xsl:when test="$name='void'">
852 <xsl:text>Void</xsl:text>
857 <xsl:when test="$name='atom'">
859 <xsl:text>Atom</xsl:text>
866 <xsl:when test="$name='forall'">
868 <xsl:when test="$charlength > $framewidth">
870 <xsl:call-template name="mksymbol">
871 <xsl:with-param name="symbol" select="$forall"/>
872 <xsl:with-param name="color" select="'blue'"/>
873 <xsl:with-param name="size" select="'+2'"/>
875 <xsl:apply-templates select="m:bvar/m:ci">
876 <xsl:with-param name="current_indent" select="$current_indent"/>
877 </xsl:apply-templates>
878 <xsl:text>:</xsl:text>
879 <xsl:apply-templates select="m:bvar/m:type">
880 <xsl:with-param name="current_indent"
881 select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
882 </xsl:apply-templates>
884 <xsl:call-template name="make_indent">
885 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
887 <xsl:text>.</xsl:text>
888 <xsl:apply-templates select="*[position()=3]">
889 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
890 </xsl:apply-templates>
893 <xsl:apply-templates mode="inline" select="."/>
899 <xsl:when test="$name='product'">
901 <xsl:when test="$charlength > $framewidth">
902 <xsl:call-template name="mksymbol">
903 <xsl:with-param name="symbol" select="$product"/>
904 <xsl:with-param name="color" select="'blue'"/>
905 <xsl:with-param name="size" select="'+2'"/>
907 <xsl:apply-templates select="m:bvar/m:ci">
908 <xsl:with-param name="current_indent" select="$current_indent"/>
909 </xsl:apply-templates>
910 <xsl:text>:</xsl:text>
911 <xsl:apply-templates select="m:bvar/m:type">
912 <xsl:with-param name="current_indent"
913 select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
914 </xsl:apply-templates><br/>
915 <xsl:call-template name="make_indent">
916 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
918 <xsl:text>.</xsl:text>
919 <xsl:apply-templates select="*[position()=3]">
920 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
921 </xsl:apply-templates>
924 <xsl:apply-templates mode="inline" select="."/>
930 <xsl:when test="$name='product_ind'">
932 <xsl:when test="$charlength > $framewidth">
934 <xsl:text>( </xsl:text>
936 <xsl:apply-templates select="m:type">
937 <xsl:with-param name="current_indent"
938 select="$current_indent + 5 + 2*string-length(m:bvar/m:ci)"/>
939 </xsl:apply-templates>
941 <xsl:call-template name="make_indent">
942 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
944 <FONT color="blue" size="+1">
945 <xsl:text> x </xsl:text>
947 <xsl:apply-templates select="*[position()=3]">
948 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
949 </xsl:apply-templates>
951 <xsl:text> )</xsl:text>
955 <xsl:apply-templates mode="inline" select="."/>
961 <xsl:when test="$name='pair'">
963 <xsl:when test="$charlength > $framewidth">
964 <FONT color="blue" size="+1">
965 <xsl:text><</xsl:text>
967 <xsl:apply-templates select="*[position()=2]">
968 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
969 </xsl:apply-templates>
970 <xsl:text>, </xsl:text>
972 <xsl:call-template name="make_indent">
973 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
975 <xsl:apply-templates select="*[position()=3]">
976 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
977 </xsl:apply-templates>
978 <FONT color="blue" size="+1">
979 <xsl:text>></xsl:text>
983 <xsl:apply-templates mode="inline" select="."/>
989 <xsl:when test="$name='union'">
991 <xsl:when test="$charlength > $framewidth">
992 <xsl:apply-templates select="*[position()=2]">
993 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
994 </xsl:apply-templates>
996 <xsl:call-template name="make_indent">
997 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
999 <FONT color="blue" size="+1">
1000 <xsl:text>+</xsl:text>
1002 <xsl:apply-templates select="*[position()=3]">
1003 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1004 </xsl:apply-templates>
1007 <xsl:apply-templates mode="inline" select="."/>
1013 <xsl:when test="$name='inl'">
1015 <xsl:when test="$charlength > $framewidth">
1017 <xsl:text>inl (</xsl:text>
1019 <xsl:apply-templates select="*[position()=2]">
1020 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1021 </xsl:apply-templates>
1023 <xsl:text> )</xsl:text>
1027 <xsl:apply-templates mode="inline" select="."/>
1033 <xsl:when test="$name='inr'">
1035 <xsl:when test="$charlength > $framewidth">
1036 <FONT color="blue" size="+1">
1037 <xsl:text>inr (</xsl:text>
1039 <xsl:apply-templates select="*[position()=2]">
1040 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1041 </xsl:apply-templates>
1042 <FONT color="blue" size="+1">
1043 <xsl:text> )</xsl:text>
1047 <xsl:apply-templates mode="inline" select="."/>
1053 <xsl:when test="$name='prop'">
1055 <xsl:text>P</xsl:text>
1057 <FONT color="blue" size="-2">
1058 <xsl:apply-templates select="m:cn">
1059 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1060 </xsl:apply-templates>
1065 <xsl:when test="$name='universe'">
1066 <FONT color="blue" size="+1">
1067 <xsl:text>U</xsl:text>
1069 <FONT color="blue" size="2">
1070 <xsl:apply-templates select="m:cn"/>
1075 <xsl:when test="$name='equal'">
1077 <xsl:when test="$charlength > $framewidth">
1078 <xsl:apply-templates select="*[position()=3]">
1079 <xsl:with-param name="current_indent" select="$current_indent"/>
1080 </xsl:apply-templates>
1082 <xsl:call-template name="make_indent">
1083 <xsl:with-param name="current_indent" select="$current_indent"/>
1084 </xsl:call-template>
1085 <FONT color="blue" size="+1">
1086 <xsl:text>= </xsl:text>
1088 <xsl:apply-templates select="*[position()=4]">
1089 <xsl:with-param name="current_indent" select="$current_indent"/>
1090 </xsl:apply-templates>
1092 <xsl:call-template name="make_indent">
1093 <xsl:with-param name="current_indent" select="$current_indent"/>
1094 </xsl:call-template>
1096 <xsl:call-template name="mksymbol">
1097 <xsl:with-param name="symbol" select="$member"/>
1098 <xsl:with-param name="color" select="'blue'"/>
1099 <xsl:with-param name="size" select="'+0'"/>
1100 </xsl:call-template>
1101 <xsl:apply-templates select="*[position()=2]">
1102 <xsl:with-param name="current_indent" select="$current_indent"/>
1103 </xsl:apply-templates>
1106 <xsl:apply-templates mode="inline" select="."/>
1113 <xsl:when test="$name='token'">
1115 <xsl:text>"</xsl:text>
1117 <xsl:apply-templates select="m:ci"/>
1119 <xsl:text>"</xsl:text>
1125 <xsl:when test="$name='nil'">
1127 <xsl:text>[]</xsl:text>
1132 <xsl:when test="$name='cons'">
1133 <xsl:apply-templates select="*[2]">
1134 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1135 </xsl:apply-templates>
1137 <xsl:call-template name="make_indent">
1138 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1139 </xsl:call-template>
1141 <xsl:text>::</xsl:text>
1143 <xsl:apply-templates select="*[3]">
1144 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1145 </xsl:apply-templates>
1151 <xsl:when test="$name='rec'">
1153 <xsl:when test="$charlength > $framewidth">
1155 <xsl:text>rectype</xsl:text>
1157 <xsl:apply-templates select="*[2]">
1158 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1159 </xsl:apply-templates>
1161 <xsl:call-template name="make_indent">
1162 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1163 </xsl:call-template>
1165 <xsl:text>=</xsl:text>
1167 <xsl:apply-templates select="*[3]">
1168 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1169 </xsl:apply-templates>
1172 <xsl:apply-templates mode="inline" select="."/>
1179 <xsl:when test="$name='t_set'">
1181 <xsl:when test="$charlength > $framewidth">
1183 <xsl:text>{</xsl:text>
1186 <xsl:when test="m:bvar/m:ci">
1187 <xsl:apply-templates select="m:bvar/m:ci"/>
1189 <xsl:text>:</xsl:text>
1191 <xsl:apply-templates select="m:bvar/m:type">
1192 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1193 </xsl:apply-templates>
1195 <xsl:call-template name="make_indent">
1196 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1197 </xsl:call-template>
1200 <xsl:apply-templates select="m:bvar/m:type">
1201 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1202 </xsl:apply-templates>
1204 <xsl:call-template name="make_indent">
1205 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1206 </xsl:call-template>
1210 <xsl:text>|</xsl:text>
1212 <xsl:apply-templates select="*[3]">
1213 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1214 </xsl:apply-templates>
1217 <xsl:text>}</xsl:text>
1222 <xsl:apply-templates mode="inline" select="."/>
1229 <xsl:when test="$name='isect'">
1230 <xsl:call-template name="mksymbol">
1231 <xsl:with-param name="symbol" select="$intersection"/>
1232 <xsl:with-param name="color" select="'blue'"/>
1233 <xsl:with-param name="size" select="'+0'"/>
1234 </xsl:call-template>
1235 <xsl:apply-templates select="m:bvar/m:ci"/>
1237 <xsl:text>:</xsl:text>
1239 <xsl:apply-templates select="m:bvar/m:type">
1240 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1241 </xsl:apply-templates>
1243 <xsl:call-template name="make_indent">
1244 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1245 </xsl:call-template>
1247 <xsl:text>.</xsl:text>
1249 <xsl:apply-templates select="*[3]">
1250 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1251 </xsl:apply-templates>
1257 <xsl:when test="$name='quotient'">
1258 <xsl:apply-templates select="m:bvar[1]"/>
1259 <xsl:text>,</xsl:text>
1260 <xsl:apply-templates select="m:bvar[2]"/>
1262 <xsl:text>:</xsl:text>
1264 <xsl:apply-templates select="*[2]">
1265 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1266 </xsl:apply-templates>
1268 <xsl:call-template name="make_indent">
1269 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1270 </xsl:call-template>
1272 <xsl:text>//</xsl:text>
1274 <xsl:apply-templates select="*[5]">
1275 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1276 </xsl:apply-templates>
1280 <!-- IF_THEN_ELSE -->
1281 <xsl:when test="$name='if_then_else'">
1283 <xsl:when test="m:where = 'atom_eq'">
1285 <xsl:text>atom_eq (</xsl:text>
1288 <xsl:when test="m:where = 'int_eq'">
1290 <xsl:text>int_eq (</xsl:text>
1293 <xsl:when test="m:where = 'less'">
1295 <xsl:text>less (</xsl:text>
1299 <xsl:apply-templates select="*[3]"/>
1300 <xsl:text>; </xsl:text>
1301 <xsl:apply-templates select="*[4]"/>
1302 <xsl:text>; </xsl:text>
1303 <xsl:apply-templates select="*[5]"/>
1304 <xsl:text>; </xsl:text>
1305 <xsl:apply-templates select="*[6]"/>
1307 <xsl:text>)</xsl:text>
1313 <xsl:when test="$name='so_lambda'">
1315 <xsl:when test="$charlength > $framewidth">
1316 <xsl:call-template name="mksymbol">
1317 <xsl:with-param name="symbol" select="$lambda"/>
1318 <xsl:with-param name="color" select="'red'"/>
1319 <xsl:with-param name="size" select="'+2'"/>
1320 </xsl:call-template>
1321 <xsl:apply-templates select="m:apply[1]/*[2]"/>
1323 <xsl:call-template name="make_indent">
1324 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1325 </xsl:call-template>
1326 <xsl:text>.</xsl:text>
1327 <xsl:apply-templates select="*[3]">
1328 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1329 </xsl:apply-templates>
1332 <xsl:apply-templates mode="inline" select="."/>
1340 <xsl:when test="$name='so_apply'">
1342 <xsl:when test="$charlength > $framewidth">
1343 <xsl:text>(</xsl:text>
1344 <xsl:apply-templates select="*[position()=2]">
1345 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1346 </xsl:apply-templates>
1347 <xsl:for-each select="*[position()>2]">
1349 <xsl:call-template name="make_indent">
1350 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1351 </xsl:call-template>
1352 <xsl:apply-templates select=".">
1353 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1354 </xsl:apply-templates>
1356 <xsl:text>)</xsl:text>
1359 <xsl:apply-templates mode="inline" select="."/>
1365 <xsl:when test="$name='app'">
1367 <xsl:when test="$charlength > $framewidth">
1368 <!-- NuPRL rendering -->
1369 <xsl:apply-templates select="*[position()=2]">
1370 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1371 </xsl:apply-templates>
1373 <xsl:call-template name="make_indent">
1374 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1375 </xsl:call-template>
1376 <xsl:if test="count(*) > 2">
1377 <xsl:text>(</xsl:text>
1378 <xsl:for-each select="*[position() > 2]">
1380 <xsl:call-template name="make_indent">
1381 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1382 </xsl:call-template>
1383 <xsl:apply-templates select="." mode="inline"/>
1384 <xsl:if test="not(position() = last())">
1385 <xsl:text>,</xsl:text>
1388 <xsl:text>)</xsl:text>
1391 <xsl:text>(</xsl:text>
1392 <xsl:apply-templates select="*[position()=2]">
1393 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1394 </xsl:apply-templates>
1395 <xsl:for-each select="*[position()>2]">
1397 <xsl:call-template name="make_indent">
1398 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1399 </xsl:call-template>
1400 <xsl:apply-templates select=".">
1401 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1402 </xsl:apply-templates>
1404 <xsl:text>)</xsl:text>
1408 <xsl:apply-templates mode="inline" select="."/>
1413 <xsl:when test="$name='cast'">
1415 <xsl:when test="$showcast = 1">
1417 <xsl:when test="$charlength > $framewidth">
1418 <xsl:text>(</xsl:text>
1419 <xsl:apply-templates select="*[position()=2]">
1420 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1421 </xsl:apply-templates><br/>
1422 <xsl:call-template name="make_indent">
1423 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1424 </xsl:call-template>
1425 <xsl:text>:</xsl:text>
1426 <xsl:apply-templates select="*[position()=3]">
1427 <xsl:with-param name="current_indent" select="$current_indent + 3"/>
1428 </xsl:apply-templates>
1429 <xsl:text>)</xsl:text>
1432 <xsl:apply-templates mode="inline" select="."/>
1437 <xsl:apply-templates select="*[position()=2]">
1438 <xsl:with-param name="current_indent" select="$current_indent"/>
1439 </xsl:apply-templates>
1443 <xsl:when test="$name='Prop'">
1444 <xsl:text>Prop</xsl:text>
1446 <xsl:when test="$name='Set'">
1447 <xsl:text>Set</xsl:text>
1449 <xsl:when test="$name='Type'">
1450 <xsl:text>Type</xsl:text>
1452 <xsl:when test="$name='mutcase'">
1454 <xsl:when test="$charlength > $framewidth">
1455 <xsl:text><</xsl:text>
1456 <xsl:apply-templates select="*[position()=2]">
1457 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1458 </xsl:apply-templates>
1459 <xsl:text>> </xsl:text>
1461 <xsl:call-template name="make_indent">
1462 <xsl:with-param name="current_indent" select="$current_indent + 2"/> </xsl:call-template>
1463 <xsl:text>CASE </xsl:text>
1464 <xsl:apply-templates select="*[position()=3]">
1465 <xsl:with-param name="current_indent" select="$current_indent + 8"/>
1466 </xsl:apply-templates>
1467 <xsl:text> OF </xsl:text>
1468 <xsl:for-each select="m:piecewise/m:piece">
1469 <!-- <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">-->
1471 <xsl:call-template name="make_indent">
1472 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1473 </xsl:call-template>
1475 <xsl:when test="position() = 1">
1476 <xsl:text>  </xsl:text>
1479 <xsl:text>| </xsl:text>
1482 <xsl:apply-templates select="./*[2]"/>
1483 <xsl:call-template name="mksymbol">
1484 <xsl:with-param name="symbol" select="$RightArrow"/>
1485 <xsl:with-param name="color" select="'green'"/>
1486 <xsl:with-param name="size" select="'+0'"/>
1487 </xsl:call-template>
1488 <xsl:variable name="body_size">
1489 <xsl:apply-templates
1490 select="./*[1]/*[1]" mode="charcount"/>
1493 <xsl:when test="$body_size > $framewidth">
1495 <xsl:call-template name="make_indent">
1496 <xsl:with-param name="current_indent"
1497 select="$current_indent + 8"/>
1498 </xsl:call-template>
1499 <xsl:apply-templates
1501 <xsl:with-param name="current_indent"
1502 select="$current_indent + 8"/>
1503 </xsl:apply-templates>
1506 <xsl:apply-templates select="./*[1]"
1513 <xsl:apply-templates mode="inline" select="."/>
1518 <xsl:when test="$name='fix'">
1520 <xsl:when test="$charlength > $framewidth">
1521 <xsl:text>FIX</xsl:text>
1522 <xsl:value-of select="m:ci"/>
1523 <xsl:text>{</xsl:text>
1524 <xsl:for-each select="m:bvar">
1526 <xsl:call-template name="make_indent">
1527 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1528 </xsl:call-template>
1529 <xsl:value-of select="m:ci"/>
1530 <xsl:text>:</xsl:text>
1531 <xsl:apply-templates select="m:type">
1532 <xsl:with-param name="current_indent"
1533 select="$current_indent + 5 + string-length(m:ci)"/>
1534 </xsl:apply-templates>
1536 <xsl:call-template name="make_indent">
1537 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1538 </xsl:call-template>
1539 <xsl:text>:=</xsl:text>
1540 <xsl:apply-templates select="following-sibling::*[position() = 1]">
1541 <xsl:with-param name="current_indent" select="$current_indent +2"/>
1542 </xsl:apply-templates>
1545 <xsl:call-template name="make_indent">
1546 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1547 </xsl:call-template>
1548 <xsl:text>}</xsl:text>
1551 <xsl:apply-templates mode="inline" select="."/>
1556 <xsl:when test="$name='cofix'">
1558 <xsl:when test="($charlength + 10) > $framewidth">
1559 <xsl:text>COFIX</xsl:text>
1560 <xsl:value-of select="m:ci"/>
1561 <xsl:text>{</xsl:text>
1563 <xsl:call-template name="make_indent">
1564 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1565 </xsl:call-template>
1566 <xsl:for-each select="m:bvar">
1567 <xsl:value-of select="m:ci"/>
1568 <xsl:text>:</xsl:text>
1569 <xsl:apply-templates select="m:type">
1570 <xsl:with-param name="current_indent"
1571 select="$current_indent + 5 + string-length(m:ci)"/>
1572 </xsl:apply-templates>
1574 <xsl:call-template name="make_indent">
1575 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1576 </xsl:call-template>
1577 <xsl:text>:=</xsl:text>
1578 <xsl:apply-templates select="following-sibling::*[position() = 1]">
1579 <xsl:with-param name="current_indent" select="$current_indent + 3"/>
1580 </xsl:apply-templates>
1584 <xsl:call-template name="make_indent">
1585 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1586 </xsl:call-template>
1587 <xsl:text>}</xsl:text>
1590 <xsl:apply-templates mode="inline" select="m:type"/>
1594 <xsl:when test="$name='let_in'">
1595 <xsl:text>let </xsl:text>
1596 <xsl:apply-templates select="m:bvar/m:ci"/>
1597 <xsl:text> := </xsl:text>
1598 <xsl:apply-templates select="*[3]">
1599 <xsl:with-param name="current_indent" select="$current_indent+14"/>
1600 </xsl:apply-templates>
1602 <xsl:call-template name="make_indent">
1603 <xsl:with-param name="current_indent" select="$current_indent"/>
1604 </xsl:call-template>
1605 <xsl:text>in </xsl:text>
1606 <xsl:apply-templates select="*[4]">
1607 <xsl:with-param name="current_indent" select="$current_indent+5"/>
1608 </xsl:apply-templates>
1611 <!-- ***************************************** -->
1612 <!-- *********** PROOF ELEMENTS ************** -->
1613 <!-- ***************************************** -->
1615 <xsl:when test="$name='proof'">
1616 <xsl:variable name="nonce" select="generate-id()"/>
1617 <xsl:variable name="freshid1" select="concat('a',$nonce)"/>
1618 <xsl:variable name="freshid2" select="concat('b',$nonce)"/>
1619 <xsl:variable name="freshid3" select="concat('c',$nonce)"/>
1620 <span ID="{$freshid1}">
1621 <xsl:apply-templates select="*[position()=2]">
1622 <xsl:with-param name="current_indent" select="$current_indent"/>
1623 </xsl:apply-templates>
1627 <xsl:when test="(preceding-sibling::*[1]/text()='letin1') or
1628 (preceding-sibling::*[1]/text()='rw_step') or
1629 (name(..)='m:lambda')">
1631 <xsl:call-template name="make_indent">
1632 <xsl:with-param name="current_indent" select="$current_indent"/>
1633 </xsl:call-template>
1634 <FONT color="red">we proved </FONT>
1638 if(document.getElementById) {
1640 <span ID="{$freshid2}">\
1641 <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>\
1643 <span ID="{$freshid3}">\
1645 <xsl:call-template name="make_indent">
1646 <xsl:with-param name="current_indent" select="$current_indent"/>
1647 </xsl:call-template>\
1648 <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>\
1651 document.to_be_deleted.push('<xsl:value-of select="$freshid1"/>');
1652 document.to_be_deleted.push('<xsl:value-of select="$freshid3"/>');
1653 document.write(' ');
1657 <xsl:call-template name="make_indent">
1658 <xsl:with-param name="current_indent" select="$current_indent"/>
1659 </xsl:call-template>\
1660 <FONT color="red">we proved </FONT>\
1666 <xsl:apply-templates select="*[position()=3]">
1667 <xsl:with-param name="current_indent" select="$current_indent + 16"/>
1668 </xsl:apply-templates>
1671 <xsl:when test="$name='side_proof'">
1672 <xsl:variable name="nonce" select="generate-id()"/>
1673 <xsl:variable name="freshid1" select="concat('a',$nonce)"/>
1674 <xsl:variable name="freshid2" select="concat('b',$nonce)"/>
1675 <xsl:variable name="freshid3" select="concat('c',$nonce)"/>
1676 <xsl:variable name="freshid4" select="concat('d',$nonce)"/>
1677 <span ID="{$freshid1}">
1678 <xsl:apply-templates select="*[position()=2]">
1679 <xsl:with-param name="current_indent" select="$current_indent"/>
1680 </xsl:apply-templates>
1684 if(document.getElementById) {
1686 <span ID="{$freshid2}">\
1687 <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>\
1689 <span ID="{$freshid3}">\
1691 <xsl:call-template name="make_indent">
1692 <xsl:with-param name="current_indent" select="$current_indent"/>
1693 </xsl:call-template>\
1694 <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>\
1697 document.to_be_deleted.push('<xsl:value-of select="$freshid1"/>');
1698 document.to_be_deleted.push('<xsl:value-of select="$freshid3"/>');
1699 document.to_be_deleted.push('<xsl:value-of select="$freshid4"/>');
1700 document.write(' ');
1704 <xsl:call-template name="make_indent">
1705 <xsl:with-param name="current_indent" select="$current_indent"/>
1706 </xsl:call-template>\
1707 <FONT color="red">we proved </FONT>\
1711 <span ID="{$freshid4}">
1712 <xsl:apply-templates select="*[position()=3]">
1713 <xsl:with-param name="current_indent" select="$current_indent + 16"/>
1714 </xsl:apply-templates>
1718 <xsl:when test="$name='eq_chain'">
1719 <FONT color="red">We have the following equality chain:</FONT>
1720 <xsl:for-each select="*[position() mod 2 = 0]">
1721 <xsl:variable name="pos" select="position()"/>
1723 <xsl:call-template name="make_indent">
1724 <xsl:with-param name="current_indent" select="$current_indent + 5"/>
1725 </xsl:call-template>
1727 <xsl:when test="$pos=1">
1728 <xsl:apply-templates select=".">
1729 <xsl:with-param name="current_indent" select="$current_indent + 5"/>
1730 </xsl:apply-templates>
1731 <xsl:text> =</xsl:text>
1734 <xsl:text>= </xsl:text>
1735 <xsl:apply-templates select=".">
1736 <xsl:with-param name="current_indent" select="$current_indent + 5"/>
1737 </xsl:apply-templates>
1740 <xsl:if test="$pos != last()">
1742 <xsl:call-template name="make_indent">
1743 <xsl:with-param name="current_indent" select="$current_indent + 15"/>
1744 </xsl:call-template>
1745 <xsl:apply-templates select="../*[position()=2*$pos +1]">
1746 <xsl:with-param name="current_indent" select="$current_indent + 15"/>
1747 </xsl:apply-templates>
1751 <!-- diseq_chain -->
1752 <xsl:when test="$name='diseq_chain'">
1753 <FONT color="red">We have the following chain of disequalities:</FONT>
1754 <xsl:for-each select="*[position() mod 3 = 2]">
1755 <xsl:variable name="pos" select="position()"/>
1757 <xsl:call-template name="make_indent">
1758 <xsl:with-param name="current_indent" select="$current_indent + 5"/>
1759 </xsl:call-template>
1761 <xsl:when test="$pos=1">
1762 <xsl:apply-templates select=".">
1763 <xsl:with-param name="current_indent" select="$current_indent + 5"/>
1764 </xsl:apply-templates>
1765 <xsl:text> </xsl:text>
1766 <xsl:apply-templates mode="inline" select="../*[position()=3*$pos]"/>
1769 <xsl:apply-templates mode="inline" select="../*[position()=3*($pos - 1)]"/>
1770 <xsl:text> </xsl:text>
1771 <xsl:apply-templates select=".">
1772 <xsl:with-param name="current_indent" select="$current_indent + 5"/>
1773 </xsl:apply-templates>
1776 <xsl:if test="$pos != last()">
1778 <xsl:call-template name="make_indent">
1779 <xsl:with-param name="current_indent" select="$current_indent + 15"/>
1780 </xsl:call-template>
1781 <xsl:apply-templates select="../*[position()=3*$pos +1]">
1782 <xsl:with-param name="current_indent" select="$current_indent + 15"/>
1783 </xsl:apply-templates>
1788 <xsl:when test="$name='letin1'">
1789 <xsl:apply-templates select="*[position()=2]">
1790 <xsl:with-param name="current_indent" select="$current_indent"/>
1791 </xsl:apply-templates>
1793 <xsl:call-template name="make_indent">
1794 <xsl:with-param name="current_indent" select="$current_indent"/>
1795 </xsl:call-template>
1796 <xsl:apply-templates select="*[position()=3]">
1797 <xsl:with-param name="current_indent" select="$current_indent"/>
1798 </xsl:apply-templates>
1801 <xsl:when test="$name='letin'">
1802 <xsl:for-each select="*[position()>1 and last()>position()]">
1803 <xsl:apply-templates select=".">
1804 <xsl:with-param name="current_indent" select="$current_indent"/>
1805 </xsl:apply-templates>
1807 <xsl:call-template name="make_indent">
1808 <xsl:with-param name="current_indent" select="$current_indent"/>
1809 </xsl:call-template>
1811 <xsl:apply-templates select="*[position()=last()]">
1812 <xsl:with-param name="current_indent" select="$current_indent"/>
1813 </xsl:apply-templates>
1816 <xsl:when test="$name='let'">
1818 <xsl:apply-templates select="m:ci"/>
1820 <xsl:apply-templates select="*[3]">
1821 <xsl:with-param name="current_indent" select="$current_indent + 7"/>
1822 </xsl:apply-templates>
1825 <xsl:when test="$name='rw_step'">
1827 <xsl:when test="name(*[2])='m:apply'">
1828 <xsl:apply-templates select="*[2]">
1829 <xsl:with-param name="current_indent" select="$current_indent"/>
1830 </xsl:apply-templates>
1833 <FONT color="red">Consider </FONT>
1834 <xsl:apply-templates select="*[2]"/>
1837 <xsl:variable name="charlength_first">
1838 <xsl:apply-templates select="*[3]" mode="root_charcount"/>
1840 <xsl:variable name="charlength_second">
1841 <xsl:apply-templates select="*[4]" mode="root_charcount"/>
1843 <xsl:variable name="charlength_side_proof">
1844 <xsl:apply-templates select="*[5]" mode="root_charcount"/>
1846 <xsl:variable name="split1"
1847 select="($charlength_first + $charlength_second) > $framewidth"/>
1848 <xsl:variable name="split2"
1849 select="($charlength_second + $charlength_side_proof) > $framewidth"/>
1850 <!-- <xsl:value-of select="$current_indent"/> -->
1851 <!-- <xsl:value-of select="string($charlength_second)"/> -->
1852 <!-- <xsl:value-of select="$charlength_side_proof"/> -->
1853 <!-- <xsl:value-of select="$split2"/> -->
1855 <xsl:call-template name="make_indent">
1856 <xsl:with-param name="current_indent" select="$current_indent"/>
1857 </xsl:call-template>
1858 <FONT color="red">Rewrite </FONT>
1859 <xsl:apply-templates mode="inline" select="*[3]"/>
1860 <xsl:text> </xsl:text>
1861 <xsl:if test="$split1">
1863 <xsl:call-template name="make_indent">
1864 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1865 </xsl:call-template>
1867 <FONT color="red">with </FONT>
1868 <xsl:apply-templates mode="inline" select="*[4]"/>
1869 <xsl:text> </xsl:text>
1870 <xsl:if test="$split2">
1872 <xsl:call-template name="make_indent">
1873 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
1874 </xsl:call-template>
1876 <FONT color="red">by </FONT>
1877 <xsl:apply-templates select="*[5]">
1878 <xsl:with-param name="current_indent" select="$current_indent+7"/>
1879 </xsl:apply-templates>
1881 <!-- rewrite and apply -->
1882 <xsl:when test="$name='rewrite_and_apply'">
1883 <xsl:apply-templates select="*[2]">
1884 <xsl:with-param name="current_indent" select="$current_indent"/>
1885 </xsl:apply-templates>
1887 <xsl:call-template name="make_indent">
1888 <xsl:with-param name="current_indent" select="$current_indent"/>
1889 </xsl:call-template>
1890 <FONT color="red">Then apply it to </FONT>
1891 <xsl:apply-templates select="*[position()>2]"/>
1893 <!-- by_induction -->
1894 <xsl:when test="$name='by_induction'">
1895 <FONT color="red">We prove </FONT>
1896 <xsl:apply-templates select="../*[3]">
1897 <xsl:with-param name="current_indent" select="$current_indent+18"/>
1898 </xsl:apply-templates>
1900 <xsl:call-template name="make_indent">
1901 <xsl:with-param name="current_indent" select="$current_indent"/>
1902 </xsl:call-template>
1903 <FONT color="red">by induction on </FONT>
1904 <xsl:apply-templates select="*[position()=last()]/*[position()=last()]">
1905 <xsl:with-param name="current_indent" select="$current_indent+30"/>
1906 </xsl:apply-templates>
1909 <xsl:call-template name="make_indent">
1910 <xsl:with-param name="current_indent" select="$current_indent"/>
1911 </xsl:call-template>
1912 <xsl:text>The induction property is</xsl:text>
1914 <xsl:call-template name="make_indent">
1915 <xsl:with-param name="current_indent" select="$current_indent"/>
1916 </xsl:call-template>
1917 <xsl:apply-templates select="*[3]">
1918 <xsl:with-param name="current_indent" select="$current_indent"/>
1919 </xsl:apply-templates>
1921 <xsl:apply-templates
1922 select="*[position()>3 and not(position()=last())]">
1923 <xsl:with-param name="current_indent" select="$current_indent+4"/>
1924 </xsl:apply-templates>
1926 <xsl:call-template name="make_indent">
1927 <xsl:with-param name="current_indent" select="$current_indent"/>
1928 </xsl:call-template>
1929 <xsl:text>End induction</xsl:text> -->
1931 <!-- inductive_case -->
1932 <xsl:when test="$name='inductive_case'">
1934 <xsl:call-template name="make_indent">
1935 <xsl:with-param name="current_indent" select="$current_indent"/>
1936 </xsl:call-template>
1937 <FONT color="red">Case </FONT>
1938 <xsl:apply-templates select="*[2]">
1939 <xsl:with-param name="current_indent" select="$current_indent +10"/>
1940 </xsl:apply-templates>
1941 <xsl:if test="*[3]/*[position()>1]">
1943 <xsl:call-template name="make_indent">
1944 <xsl:with-param name="current_indent" select="$current_indent+4"/>
1945 </xsl:call-template>
1946 <FONT color="red">By induction hypothesis, we have:</FONT>
1947 <xsl:for-each select="*[3]/*[position()>1]">
1949 <xsl:call-template name="make_indent">
1950 <xsl:with-param name="current_indent" select="$current_indent + 4"/>
1951 </xsl:call-template>
1952 <xsl:text>(</xsl:text>
1953 <xsl:apply-templates select="m:ci"/>
1954 <xsl:text>) </xsl:text>
1955 <xsl:apply-templates select="m:type">
1956 <xsl:with-param name="current_indent" select="$current_indent + 8"/>
1957 </xsl:apply-templates>
1961 <xsl:call-template name="make_indent">
1962 <xsl:with-param name="current_indent" select="$current_indent + 4"/>
1963 </xsl:call-template>
1964 <xsl:apply-templates select="*[4]">
1965 <xsl:with-param name="current_indent" select="$current_indent +4"/>
1966 </xsl:apply-templates>
1968 <xsl:call-template name="make_indent">
1969 <xsl:with-param name="current_indent" select="$current_indent"/>
1970 </xsl:call-template>
1971 <xsl:text>End Case</xsl:text> -->
1974 <xsl:when test="$name='case_lhs'">
1976 <xsl:when test="count(*)=2">
1977 <xsl:apply-templates mode="inline" select="*[2]"/>
1980 <xsl:text>(</xsl:text>
1981 <xsl:apply-templates mode="inline" select="*[2]"/>
1982 <xsl:for-each select="m:bvar">
1983 <xsl:text> </xsl:text>
1984 <xsl:apply-templates mode="inline" select="*[1]"/>
1985 <xsl:text>:</xsl:text>
1986 <xsl:apply-templates mode="inline" select="m:type/*[1]"/>
1988 <xsl:text>)</xsl:text>
1993 <xsl:when test="$name='false_ind'">
1994 <xsl:apply-templates select="*[3]">
1995 <xsl:with-param name="current_indent" select="$current_indent"/>
1996 </xsl:apply-templates>
1998 <xsl:call-template name="make_indent">
1999 <xsl:with-param name="current_indent" select="$current_indent"/>
2000 </xsl:call-template>
2001 <FONT color="red">Contradiction.</FONT>
2004 <xsl:when test="$name='and_ind'">
2006 <xsl:when test="name(*[2])='m:apply'">
2007 <xsl:apply-templates select="*[2]">
2008 <xsl:with-param name="current_indent" select="$current_indent"/>
2009 </xsl:apply-templates>
2012 <FONT color="red">Consider </FONT>
2013 <xsl:apply-templates select="*[2]"/>
2017 <xsl:call-template name="make_indent">
2018 <xsl:with-param name="current_indent" select="$current_indent"/>
2019 </xsl:call-template>
2020 <FONT color="red">In particular, we have</FONT>
2022 <xsl:call-template name="make_indent">
2023 <xsl:with-param name="current_indent" select="$current_indent"/>
2024 </xsl:call-template>
2026 <xsl:apply-templates select="*[3]"/>
2028 <xsl:apply-templates select="*[4]">
2029 <xsl:with-param name="current_indent" select="$current_indent + 9"/>
2030 </xsl:apply-templates>
2032 <xsl:call-template name="make_indent">
2033 <xsl:with-param name="current_indent" select="$current_indent"/>
2034 </xsl:call-template>
2036 <xsl:apply-templates select="*[5]"/>
2038 <xsl:apply-templates select="*[6]">
2039 <xsl:with-param name="current_indent" select="$current_indent + 9"/>
2040 </xsl:apply-templates>
2042 <xsl:call-template name="make_indent">
2043 <xsl:with-param name="current_indent" select="$current_indent"/>
2044 </xsl:call-template>
2045 <xsl:apply-templates select="*[7]">
2046 <xsl:with-param name="current_indent" select="$current_indent"/>
2047 </xsl:apply-templates>
2049 <!-- full_or_ind -->
2050 <xsl:when test="$name='full_or_ind'">
2052 <xsl:when test="name(*[2])='m:apply'">
2053 <xsl:apply-templates select="*[2]">
2054 <xsl:with-param name="current_indent" select="$current_indent"/>
2055 </xsl:apply-templates>
2058 <FONT color="red">Consider </FONT>
2059 <xsl:apply-templates select="*[2]"/>
2063 <xsl:call-template name="make_indent">
2064 <xsl:with-param name="current_indent" select="$current_indent"/>
2065 </xsl:call-template>
2066 <FONT color="red">We proceed by cases to prove </FONT>
2067 <xsl:apply-templates select="*[3]"/>
2069 <xsl:call-template name="make_indent">
2070 <xsl:with-param name="current_indent" select="$current_indent+4"/>
2071 </xsl:call-template>
2072 <FONT color="red">Left: suppose </FONT>
2073 <xsl:text>(</xsl:text>
2074 <xsl:value-of select="*[4]/m:bvar/m:ci"/>
2075 <xsl:text>) </xsl:text>
2076 <xsl:apply-templates
2077 select="*[4]/m:bvar/m:type/*[1]"/>
2079 <xsl:call-template name="make_indent">
2080 <xsl:with-param name="current_indent" select="$current_indent+15"/>
2081 </xsl:call-template>
2082 <xsl:apply-templates
2084 <xsl:with-param name="current_indent" select="$current_indent+15"/>
2085 </xsl:apply-templates>
2087 <xsl:call-template name="make_indent">
2088 <xsl:with-param name="current_indent" select="$current_indent+4"/>
2089 </xsl:call-template>
2090 <FONT color="red">Right: suppose </FONT>
2091 <xsl:text>(</xsl:text>
2092 <xsl:value-of select="*[5]/m:bvar/m:ci"/>
2093 <xsl:text>) </xsl:text>
2094 <xsl:apply-templates
2095 select="*[5]/m:bvar/m:type/*[1]"/>
2097 <xsl:call-template name="make_indent">
2098 <xsl:with-param name="current_indent" select="$current_indent+16"/>
2099 </xsl:call-template>
2100 <xsl:apply-templates
2102 <xsl:with-param name="current_indent" select="$current_indent+16"/>
2103 </xsl:apply-templates>
2106 <xsl:when test="$name='or_ind'">
2108 <xsl:when test="name(*[2])='m:apply'">
2109 <xsl:apply-templates select="*[2]">
2110 <xsl:with-param name="current_indent" select="$current_indent"/>
2111 </xsl:apply-templates>
2114 <FONT color="red">Consider </FONT>
2115 <xsl:apply-templates select="*[2]"/>
2119 <xsl:call-template name="make_indent">
2120 <xsl:with-param name="current_indent" select="$current_indent"/>
2121 </xsl:call-template>
2122 <FONT color="red">We prove </FONT>
2123 <xsl:apply-templates select="*[3]"/>
2124 <FONT color="red"> by cases:</FONT>
2126 <xsl:call-template name="make_indent">
2127 <xsl:with-param name="current_indent" select="$current_indent"/>
2128 </xsl:call-template>
2130 <xsl:apply-templates select="*[4]">
2131 <xsl:with-param name="current_indent" select="$current_indent"/>
2132 </xsl:apply-templates>
2134 <xsl:call-template name="make_indent">
2135 <xsl:with-param name="current_indent" select="$current_indent"/>
2136 </xsl:call-template>
2138 <xsl:apply-templates select="*[5]">
2139 <xsl:with-param name="current_indent" select="$current_indent"/>
2140 </xsl:apply-templates>
2143 <xsl:when test="$name='ex_ind'">
2145 <xsl:when test="name(*[2])='m:apply'">
2146 <xsl:apply-templates select="*[2]">
2147 <xsl:with-param name="current_indent" select="$current_indent"/>
2148 </xsl:apply-templates>
2151 <FONT color="red">Consider </FONT>
2152 <xsl:apply-templates select="*[2]">
2153 <xsl:with-param name="current_indent" select="$current_indent"/>
2154 </xsl:apply-templates>
2158 <xsl:call-template name="make_indent">
2159 <xsl:with-param name="current_indent" select="$current_indent"/>
2160 </xsl:call-template>
2161 <FONT color="red">Let </FONT>
2162 <xsl:apply-templates mode="inline" select="*[3]"/>
2164 <xsl:apply-templates mode="inline" select="*[4]"/>
2165 <FONT color="red"> such that</FONT>
2167 <xsl:call-template name="make_indent">
2168 <xsl:with-param name="current_indent" select="$current_indent"/>
2169 </xsl:call-template>
2171 <xsl:apply-templates mode="inline" select="*[5]"/>
2173 <xsl:apply-templates select="*[6]">
2174 <xsl:with-param name="current_indent" select="$current_indent +7"/>
2175 </xsl:apply-templates>
2177 <xsl:call-template name="make_indent">
2178 <xsl:with-param name="current_indent" select="$current_indent"/>
2179 </xsl:call-template>
2180 <xsl:apply-templates select="*[7]">
2181 <xsl:with-param name="current_indent" select="$current_indent"/>
2182 </xsl:apply-templates>
2189 <xsl:template match="m:lambda">
2190 <xsl:param name="current_indent" select="0"/>
2191 <xsl:variable name="charlength">
2192 <xsl:apply-templates select="*[position()=1]" mode="charcount"/>
2193 <!-- <xsl:apply-templates select="." mode="charcount"/> -->
2195 <!-- <xsl:value-of select="$charlength"/> -->
2196 <!-- <xsl:value-of select="$current_indent"/> -->
2198 <xsl:when test="$charlength > $framewidth">
2200 <xsl:call-template name="mksymbol">
2201 <xsl:with-param name="symbol" select="$lambda"/>
2202 <xsl:with-param name="color" select="'red'"/>
2203 <xsl:with-param name="size" select="'+2'"/>
2204 </xsl:call-template>
2205 <xsl:apply-templates select="m:bvar/m:ci"/>
2206 <xsl:text>:</xsl:text>
2207 <xsl:apply-templates select="m:bvar/m:type">
2208 <xsl:with-param name="current_indent"
2209 select="$current_indent + 4 + 2*string-length(m:bvar/m:ci)"/>
2210 </xsl:apply-templates><br/>
2211 <xsl:call-template name="make_indent">
2212 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
2213 </xsl:call-template>
2214 <xsl:text>.</xsl:text>
2215 <xsl:apply-templates select="*[position()=2]">
2216 <xsl:with-param name="current_indent" select="$current_indent + 2"/>
2217 </xsl:apply-templates>
2220 <xsl:apply-templates mode="inline" select="."/>
2226 <xsl:template match="m:ci">
2228 <xsl:when test="boolean(@definitionURL)">
2229 <a href="{@definitionURL}">
2230 <xsl:apply-templates/>
2234 <xsl:value-of select="."/>
2239 <!-- CHAR COUNTING -->
2241 <!-- enter this counting mode selecting the root -->
2242 <xsl:template match="*" mode="root_charcount">
2243 <xsl:param name="incurrent_length" select="0"/>
2245 <xsl:when test="count(*)=0">
2246 <xsl:value-of select="0"/>
2248 <xsl:when test="name()='m:ci'">
2249 <xsl:value-of select="string-length()"/>
2252 <xsl:apply-templates select="*[1]" mode="charcount">
2253 <xsl:with-param name="incurrent_length" select="$incurrent_length"/>
2254 </xsl:apply-templates>
2260 <!-- CASI PARTICOLARI MODE=INLINE -->
2262 <xsl:template mode="inline" match="m:interval">
2264 <xsl:text>[</xsl:text>
2266 <xsl:apply-templates select="*[1]"/>
2267 <xsl:text>, </xsl:text>
2268 <xsl:apply-templates select="*[2]"/>
2270 <xsl:text>]</xsl:text>
2274 <xsl:template mode="inline" match="m:apply[m:in]">
2275 <xsl:apply-templates select="*[2]"/>
2276 <xsl:text> </xsl:text>
2277 <xsl:call-template name="mksymbol">
2278 <xsl:with-param name="symbol" select="$member"/>
2279 <xsl:with-param name="color" select="'blue'"/>
2280 <xsl:with-param name="size" select="'+0'"/>
2281 </xsl:call-template>
2282 <xsl:text> </xsl:text>
2283 <xsl:apply-templates select="*[3]"/>
2286 <xsl:template mode="inline" match="m:integers">
2287 <xsl:call-template name="mksymbol">
2288 <xsl:with-param name="symbol" select="$integers"/>
2289 <xsl:with-param name="color" select="'blue'"/>
2290 <xsl:with-param name="size" select="'+0'"/>
2291 </xsl:call-template>
2294 <xsl:template mode="inline" match="m:naturalnumbers">
2295 <xsl:call-template name="mksymbol">
2296 <xsl:with-param name="symbol" select="$naturalnumbers"/>
2297 <xsl:with-param name="size" select="'+0'"/>
2298 </xsl:call-template>
2301 <xsl:template mode="inline" match="m:apply[m:implies]">
2302 <xsl:text>(</xsl:text>
2303 <xsl:apply-templates select="*[2]"/>
2304 <xsl:text> </xsl:text>
2305 <xsl:call-template name="mksymbol">
2306 <xsl:with-param name="symbol" select="$implies"/>
2307 <xsl:with-param name="color" select="'blue'"/>
2308 <xsl:with-param name="size" select="'+0'"/>
2309 </xsl:call-template>
2310 <xsl:text> </xsl:text>
2311 <xsl:apply-templates select="*[3]"/>
2312 <xsl:text>)</xsl:text>
2315 <xsl:template mode="inline" match="m:apply[m:exists]">
2316 <xsl:call-template name="mksymbol">
2317 <xsl:with-param name="symbol" select="$NUPRLexists"/>
2318 <xsl:with-param name="color" select="'blue'"/>
2319 <xsl:with-param name="size" select="'+0'"/>
2320 </xsl:call-template>
2321 <xsl:apply-templates select="m:bvar/m:ci"/>
2322 <xsl:text>:</xsl:text>
2323 <xsl:apply-templates select="m:condition/*"/>
2324 <!-- CSC: old wrong code
2325 <xsl:if test="count(m:condition/m:apply/*[3]) > 1">
2326 <xsl:text>(</xsl:text>
2328 <xsl:apply-templates select="m:condition/m:apply/*[3]"/>
2329 <xsl:if test="count(m:bvar/m:type/m:apply/*[3]) > 1">
2330 <xsl:text>)</xsl:text>
2333 <xsl:text>.</xsl:text>
2334 <xsl:apply-templates select="*[position()=4]"/>
2339 <xsl:template mode="inline" match="m:apply/*[m:ci][position()=1]">
2340 <xsl:apply-templates select="*[1]"/>
2341 <xsl:text>(</xsl:text>
2342 <xsl:for-each select="*[position()>1 and position()!=last()]">
2343 <xsl:apply-templates/>
2344 <xsl:text>, </xsl:text>
2346 <xsl:apply-templates select="*[position()=last()]"/>
2347 <xsl:text>)</xsl:text>
2350 <!-- CASI PARTICOLARI NON IN LINE -->
2352 <xsl:template match="m:interval">
2354 <xsl:text>[</xsl:text>
2356 <xsl:apply-templates select="*[1]"/>
2357 <xsl:text>, </xsl:text>
2358 <xsl:apply-templates select="*[2]"/>
2360 <xsl:text>]</xsl:text>
2364 <!--<xsl:param name="current_indent" select="0"/>
2365 <xsl:variable name="charlength">
2366 <xsl:apply-templates select="." mode="charcount"/>
2369 <xsl:when test="$charlength > $framewidth">
2371 <xsl:text>[</xsl:text>
2373 <xsl:apply-templates select="*[1]">
2374 <xsl:with-param name="current_indent" select="$current_indent"/>
2375 </xsl:apply-templates>
2376 <xsl:text>, </xsl:text>
2378 <xsl:call-template name="make_indent">
2379 <xsl:with-param name="current_indent" select="$current_indent"/>
2380 </xsl:call-template>
2381 <xsl:apply-templates select="*[2]">
2382 <xsl:with-param name="current_indent" select="$current_indent"/>
2383 </xsl:apply-templates>
2385 <xsl:text>]</xsl:text>
2393 <xsl:template match="m:apply[m:in]">
2394 <xsl:param name="current_indent" select="0"/>
2395 <xsl:variable name="charlength">
2396 <xsl:apply-templates select="m:in" mode="charcount"/>
2399 <xsl:when test="$charlength > $framewidth">
2400 <xsl:apply-templates select="*[2]">
2401 <xsl:with-param name="current_indent" select="$current_indent"/>
2402 </xsl:apply-templates>
2404 <xsl:call-template name="make_indent">
2405 <xsl:with-param name="current_indent" select="$current_indent"/>
2406 </xsl:call-template>
2407 <xsl:call-template name="mksymbol">
2408 <xsl:with-param name="symbol" select="$member"/>
2409 <xsl:with-param name="color" select="'blue'"/>
2410 <xsl:with-param name="size" select="'+0'"/>
2411 </xsl:call-template>
2412 <xsl:text> </xsl:text>
2413 <xsl:apply-templates select="*[3]">
2414 <xsl:with-param name="current_indent" select="$current_indent"/>
2415 </xsl:apply-templates>
2418 <xsl:apply-templates mode="inline" select="."/>
2423 <xsl:template match="m:integers">
2424 <xsl:call-template name="mksymbol">
2425 <xsl:with-param name="symbol" select="$integers"/>
2426 <xsl:with-param name="color" select="'blue'"/>
2427 <xsl:with-param name="size" select="'+0'"/>
2428 </xsl:call-template>
2431 <xsl:template match="m:naturalnumbers">
2432 <xsl:call-template name="mksymbol">
2433 <xsl:with-param name="symbol" select="$naturalnumbers"/>
2434 <xsl:with-param name="size" select="'+0'"/>
2435 </xsl:call-template>
2438 <xsl:template match="m:apply[m:implies]">
2439 <xsl:param name="current_indent" select="0"/>
2440 <xsl:variable name="charlength">
2441 <xsl:apply-templates select="m:implies" mode="charcount"/>
2444 <xsl:when test="$charlength > $framewidth">
2445 <xsl:text>implies</xsl:text>
2446 <xsl:text>(</xsl:text>
2447 <xsl:apply-templates select="*[2]">
2448 <xsl:with-param name="current_indent" select="$current_indent"/>
2449 </xsl:apply-templates>
2451 <xsl:call-template name="make_indent">
2452 <xsl:with-param name="current_indent" select="$current_indent"/>
2453 </xsl:call-template>
2454 <xsl:call-template name="mksymbol">
2455 <xsl:with-param name="symbol" select="$implies"/>
2456 <xsl:with-param name="color" select="'blue'"/>
2457 <xsl:with-param name="size" select="'+0'"/>
2458 </xsl:call-template>
2459 <xsl:text> </xsl:text>
2460 <xsl:apply-templates select="*[3]">
2461 <xsl:with-param name="current_indent" select="$current_indent"/>
2462 </xsl:apply-templates>
2463 <xsl:text>)</xsl:text>
2466 <xsl:apply-templates mode="inline" select="."/>
2471 <xsl:template match="m:apply[m:exists]">
2472 <xsl:param name="current_indent" select="0"/>
2473 <xsl:variable name="charlength">
2474 <xsl:apply-templates select="m:implies" mode="charcount"/>
2477 <xsl:when test="$charlength > $framewidth">
2478 <xsl:call-template name="mksymbol">
2479 <xsl:with-param name="symbol" select="$NUPRLexists"/>
2480 <xsl:with-param name="color" select="'blue'"/>
2481 <xsl:with-param name="size" select="'+0'"/>
2482 </xsl:call-template>
2483 <xsl:apply-templates select="m:bvar/m:ci"/>
2484 <xsl:text>:</xsl:text>
2485 <!--<xsl:if test="count(m:condition/m:apply/*[3]) > 1">
2486 <xsl:text>(</xsl:text>
2488 <xsl:apply-templates select="m:condition/m:apply/*[3]">
2489 <xsl:with-param name="current_indent" select="$current_indent"/>
2490 </xsl:apply-templates>
2491 <!--<xsl:if test="count(m:bvar/m:type/m:apply/*[3]) > 1">
2492 <xsl:text>)</xsl:text>
2495 <xsl:call-template name="make_indent">
2496 <xsl:with-param name="current_indent" select="$current_indent"/>
2497 </xsl:call-template>
2498 <xsl:text>.</xsl:text>
2499 <xsl:apply-templates select="*[position()=4]">
2500 <xsl:with-param name="current_indent" select="$current_indent"/>
2501 </xsl:apply-templates>
2504 <xsl:apply-templates mode="inline" select="."/>
2510 <xsl:template match="m:apply/m:ci">
2511 <xsl:apply-templates/>
2512 <xsl:text>(</xsl:text>
2513 <xsl:for-each select="*[position()>1 and position()!=last()]">
2514 <xsl:apply-templates/>
2515 <xsl:text>, </xsl:text>
2517 <xsl:apply-templates select="*[position()=last()]"/>
2518 <xsl:text>)</xsl:text>
2521 <!-- enter this mode selecting the first child -->
2523 <xsl:template match="m:ci|m:csymbol|m:implies|m:exists|m:interval|m:in" mode="charcount">
2524 <xsl:param name="incurrent_length" select="0"/>
2526 <xsl:when test="$framewidth >= ($incurrent_length + string-length())">
2527 <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>
2529 <xsl:when test="string($siblength) = """>
2530 <xsl:value-of select="$incurrent_length + string-length()"/>
2533 <xsl:value-of select="number($siblength)"/>
2538 <xsl:value-of select="$incurrent_length + string-length()"/>
2543 <xsl:template match="*" mode="charcount">
2544 <xsl:param name="incurrent_length" select="0"/>
2546 <xsl:when test="count(child::*) = 0">
2547 <xsl:value-of select="$incurrent_length"/>
2550 <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>
2552 <xsl:when test="$framewidth >= number($childlength)">
2553 <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>
2555 <xsl:when test="string($siblength) = """>
2556 <xsl:value-of select="number($childlength)"/>
2559 <xsl:value-of select="number($siblength)"/>
2564 <xsl:value-of select="number($childlength)"/>
2572 <!--***********************************************************************-->
2574 <!--***********************************************************************-->
2578 <xsl:template match="Rule">
2579 <xsl:param name="current_indent" select="0"/>
2581 <xsl:variable name="char">
2582 <xsl:value-of select="m:apply"/>
2584 <xsl:variable name="length" select="string-length($char)"/>
2587 <xsl:call-template name="make_indent">
2588 <xsl:with-param name="current_indent" select="$current_indent"/>
2589 </xsl:call-template>
2590 <FONT color="red">Rule: </FONT>
2592 <xsl:when test="m:ci">
2594 <xsl:apply-templates>
2595 <xsl:with-param name="current_indent" select="$current_indent"/>
2596 </xsl:apply-templates>
2601 <xsl:when test="$length > $framewidth">
2603 <xsl:call-template name="make_indent">
2604 <xsl:with-param name="current_indent" select="$current_indent"/>
2605 </xsl:call-template>
2606 <xsl:variable name="char_rule">
2607 <xsl:value-of select="m:apply/*[1]"/>
2609 <xsl:variable name="length_rule" select="string-length($char_rule)"/>
2611 <xsl:apply-templates select="m:apply/*[1]">
2612 <xsl:with-param name="current_indent" select="$current_indent"/>
2613 </xsl:apply-templates>
2614 <xsl:if test="count(m:apply/*)>2">
2616 <xsl:call-template name="make_indent">
2617 <xsl:with-param name="current_indent" select="$current_indent + $length_rule"/>
2618 </xsl:call-template>
2621 <xsl:text> ( </xsl:text>
2624 <xsl:for-each select="m:apply/*[position()!=1]">
2625 <xsl:if test="position()!=1">
2626 <xsl:call-template name="make_indent">
2627 <xsl:with-param name="current_indent" select="$current_indent + $length_rule"/>
2628 </xsl:call-template>
2631 <xsl:when test="*[1]='level-exp'">
2632 <xsl:text>level-exp(</xsl:text>
2633 <xsl:apply-templates select="*[2]">
2634 <xsl:with-param name="current_indent" select="$current_indent"/>
2635 </xsl:apply-templates>
2636 <xsl:text>)</xsl:text>
2638 <xsl:when test="m:apply">
2639 <xsl:apply-templates select=".">
2640 <xsl:with-param name="current_indent" select="$current_indent"/>
2641 </xsl:apply-templates>
2644 <xsl:apply-templates>
2645 <xsl:with-param name="current_indent" select="$current_indent"/>
2646 </xsl:apply-templates>
2649 <xsl:if test="position()!=last()">
2650 <xsl:text>, </xsl:text>
2655 <xsl:text> )</xsl:text>
2661 <xsl:apply-templates select="m:apply/*[1]">
2662 <xsl:with-param name="current_indent" select="$current_indent"/>
2663 </xsl:apply-templates>
2666 <xsl:text> ( </xsl:text>
2669 <xsl:for-each select="m:apply/*[position()!=1]">
2671 <xsl:when test="*[1]='level-exp'">
2672 <xsl:text>level-exp(</xsl:text>
2673 <xsl:apply-templates select="*[2]">
2674 <xsl:with-param name="current_indent" select="$current_indent"/>
2675 </xsl:apply-templates>
2676 <xsl:text>)</xsl:text>
2678 <xsl:when test="m:apply">
2679 <xsl:apply-templates select=".">
2680 <xsl:with-param name="current_indent" select="$current_indent"/>
2681 </xsl:apply-templates>
2685 <xsl:apply-templates>
2686 <xsl:with-param name="current_indent" select="$current_indent"/>
2687 </xsl:apply-templates>
2690 <xsl:if test="position()!=last()">
2691 <xsl:text>, </xsl:text>
2695 <xsl:text> )</xsl:text>
2706 <xsl:template match="Sequent">
2707 <xsl:param name="current_indent" select="0"/>
2708 <xsl:call-template name="make_indent">
2709 <xsl:with-param name="current_indent" select="$current_indent"/>
2710 </xsl:call-template>
2711 <FONT color="red">Sequent <xsl:value-of select="@id"/></FONT>
2714 <xsl:for-each select="Decl">
2715 <xsl:variable name="num" select="position()"/>
2716 <xsl:call-template name="make_indent">
2717 <xsl:with-param name="current_indent" select="$current_indent"/>
2718 </xsl:call-template>
2719 <xsl:value-of select="$num"/>
2720 <xsl:text>) </xsl:text>
2721 <xsl:if test="@name">
2722 <FONT color="green">
2723 <xsl:value-of select="@name"/>
2724 <xsl:text>:</xsl:text>
2728 <xsl:apply-templates>
2729 <xsl:with-param name="current_indent" select="$current_indent + 10"/>
2730 </xsl:apply-templates>
2732 <xsl:when test="m:apply">
2733 <xsl:apply-templates select=".">
2734 <xsl:with-param name="current_indent" select="$current_indent"/>
2735 </xsl:apply-templates>
2738 <xsl:apply-templates>
2739 <xsl:with-param name="current_indent" select="$current_indent"/>
2740 </xsl:apply-templates>
2745 <xsl:call-template name="make_indent">
2746 <xsl:with-param name="current_indent" select="$current_indent"/>
2747 </xsl:call-template>
2749 <FONT color="red" size="+1">|- </FONT>
2751 <xsl:call-template name="make_indent">
2752 <xsl:with-param name="current_indent" select="$current_indent"/>
2753 </xsl:call-template>
2754 <xsl:apply-templates select="Goal/*">
2755 <xsl:with-param name="current_indent" select="$current_indent"/>
2756 </xsl:apply-templates>
2761 <xsl:template match="Node">
2762 <xsl:param name="current_indent" select="0"/>
2764 <xsl:variable name="nonce" select="generate-id()"/>
2765 <xsl:variable name="freshid2" select="concat('b',$nonce)"/>
2766 <xsl:variable name="freshid3" select="concat('c',$nonce)"/>
2767 <xsl:variable name="freshid4" select="concat('d',$nonce)"/>
2768 <xsl:variable name="freshid5" select="concat('e',$nonce)"/>
2770 <xsl:apply-templates select="Sequent">
2771 <xsl:with-param name="current_indent" select="$current_indent"/>
2772 </xsl:apply-templates>
2774 <xsl:when test="Rule">
2775 <xsl:apply-templates select="Rule">
2776 <xsl:with-param name="current_indent" select="$current_indent"/>
2777 </xsl:apply-templates>
2779 <xsl:when test="TacticInstance">
2783 <xsl:call-template name="make_indent">
2784 <xsl:with-param name="current_indent" select="$current_indent"/>
2785 </xsl:call-template>
2786 <xsl:text>By </xsl:text>
2787 <xsl:apply-templates select="TacticInstance/@name"/>
2788 <a style="text-decoration:underline ; color:green" href="{TacticInstance/@uri}">Tactic Details</a>
2789 <xsl:if test="$explode_tactics">
2790 <span ID="{$freshid4}">
2791 <a style="text-decoration:underline ; color:green" href="" onClick="Hide(document.getElementById('{$freshid4}'));Show(document.getElementById('{$freshid5}'));return (0==1);">Details</a>
2795 <xsl:if test="$explode_tactics">
2796 <div ID="{$freshid5}">
2797 <xsl:call-template name="make_indent">
2798 <xsl:with-param name="current_indent" select="$current_indent"/>
2799 </xsl:call-template>
2800 <a style="text-decoration:underline ; color:red" href="" onClick="Show(document.getElementById('{$freshid4}'));Hide(document.getElementById('{$freshid5}'));return (0==1);">Hide details</a>
2802 <xsl:apply-templates select="TacticProof">
2803 <xsl:with-param name="current_indent" select="$current_indent + 5"/>
2804 </xsl:apply-templates>
2810 <xsl:if test="count(Node)!=0">
2812 <xsl:when test="count(Node)=1">
2813 <span ID="{$freshid2}">
2814 <xsl:call-template name="make_indent">
2815 <xsl:with-param name="current_indent" select="$current_indent"/>
2816 </xsl:call-template>
2817 <a style="text-decoration:underline ; color:green" href="" onClick="Hide(document.getElementById('{$freshid2}'));Show(document.getElementById('{$freshid3}'));return (0==1);">Subgoal</a>
2822 <span ID="{$freshid2}">
2823 <xsl:call-template name="make_indent">
2824 <xsl:with-param name="current_indent" select="$current_indent"/>
2825 </xsl:call-template>
2826 <a style="text-decoration:underline ; color:green" href="" onClick="Hide(document.getElementById('{$freshid2}'));Show(document.getElementById('{$freshid3}'));return (0==1);">Subgoals</a>
2831 <div ID="{$freshid3}">
2832 <xsl:call-template name="make_indent">
2833 <xsl:with-param name="current_indent" select="$current_indent"/>
2834 </xsl:call-template>
2835 <a style="text-decoration:underline ; color:red" href="" onClick="Show(document.getElementById('{$freshid2}'));Hide(document.getElementById('{$freshid3}'));return (0==1);">Back</a>
2837 <xsl:apply-templates select="Node">
2838 <xsl:with-param name="current_indent" select="$current_indent + 5"/>
2839 </xsl:apply-templates>
2842 document.to_be_deleted.push('<xsl:value-of select="$freshid3"/>');
2847 <!-- NuPRLDefinition -->
2849 <xsl:template match="NuPrlDefinition">
2850 <xsl:apply-templates select="*[1]"/>
2851 <xsl:text> := </xsl:text>
2852 <xsl:apply-templates select="*[2]"/>
2857 <xsl:template match="Definition">
2858 <xsl:param name="current_indent" select="0"/>
2860 DEFINITION <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != """><xsl:value-of select="Params"/></xsl:if>)<br/>
2862 <xsl:call-template name="make_indent">
2863 <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2864 </xsl:call-template>
2865 <xsl:apply-templates select="type/*[1]">
2866 <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2867 </xsl:apply-templates><br/>
2869 <xsl:call-template name="make_indent">
2870 <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2871 </xsl:call-template>
2872 <xsl:apply-templates select="body/Node">
2873 <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2874 </xsl:apply-templates>
2880 <xsl:template match="Axiom">
2881 <xsl:param name="current_indent" select="0"/>
2883 AXIOM <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != """><xsl:value-of select="Params"/></xsl:if>)<br/>
2885 <xsl:call-template name="make_indent">
2886 <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2887 </xsl:call-template>
2888 <xsl:apply-templates select="type/*[1]">
2889 <xsl:with-param name="current_indent" select="$current_indent + 7"/>
2890 </xsl:apply-templates>
2894 <!-- UNFINISHED PROOF -->
2896 <xsl:template match="CurrentProof">
2897 <xsl:param name="current_indent" select="0"/>
2899 UNFINISHED PROOF <xsl:value-of select="@name"/>(<xsl:if test="string(./Params) != """><xsl:value-of select="Params"/></xsl:if>)<br/>
2900 THESIS: <xsl:apply-templates select="type/*[1]">
2901 <xsl:with-param name="current_indent" select="$current_indent + 8"/>
2902 </xsl:apply-templates><br/>
2904 <xsl:for-each select="Conjecture">
2906 <xsl:call-template name="make_indent">
2907 <xsl:with-param name="current_indent" select="$current_indent + 8"/>
2908 </xsl:call-template>
2909 <xsl:for-each select="Decl|Def|Hidden">
2911 <xsl:when test="name(.)='Decl'">
2913 <xsl:when test="@name">
2914 <xsl:value-of select="@name"/>
2917 <xsl:text>_</xsl:text>
2920 <xsl:text> : </xsl:text>
2921 <xsl:apply-templates select="./*[1]">
2922 <xsl:with-param name="current_indent" select="$current_indent"/>
2923 </xsl:apply-templates>
2925 <xsl:when test="name(.)='Def'">
2927 <xsl:when test="@name">
2928 <xsl:value-of select="@name"/>
2931 <xsl:text>_</xsl:text>
2934 <xsl:text> := </xsl:text>
2935 <xsl:apply-templates select="./*[1]">
2936 <xsl:with-param name="current_indent" select="$current_indent"/>
2937 </xsl:apply-templates>
2940 <xsl:text> _ :? _ </xsl:text>
2944 |- <xsl:value-of select="./@no"/> :
2945 <xsl:apply-templates select="./Goal/*[1]">
2946 <xsl:with-param name="current_indent" select="$current_indent + 11"/>
2947 </xsl:apply-templates>
2951 <xsl:apply-templates select="body/*[1]">
2952 <xsl:with-param name="current_indent" select="$current_indent + 8"/>
2953 </xsl:apply-templates>
2957 <!-- MUTUAL INDUCTIVE DEFINITION -->
2959 <xsl:template match="InductiveDefinition">
2960 <xsl:param name="current_indent" select="0"/>
2962 <xsl:for-each select="InductiveType">
2964 <xsl:when test="position() = 1">
2966 <xsl:when test="string(./@inductive) = "true"">
2967 INDUCTIVE DEFINITION
2970 COINDUCTIVE DEFINITION
2978 <xsl:value-of select="./@name"/>(<xsl:if test="string(../Params) != """><xsl:value-of select="../Params"/></xsl:if>)
2980 <xsl:if test="string(../Param) != """>
2981 <xsl:for-each select="../Param">
2982 <xsl:value-of select="./@name"/>
2984 <xsl:apply-templates select="*"/>
2989 <xsl:apply-templates select="./arity/*[1]">
2990 <xsl:with-param name="current_indent" select="$current_indent + 9"/>
2991 </xsl:apply-templates> <br/>
2993 <xsl:for-each select="./Constructor">
2995 <xsl:call-template name="make_indent">
2996 <xsl:with-param name="current_indent" select="$current_indent + 3"/>
2997 </xsl:call-template>
2999 <xsl:when test="position() = 1">
3000 <xsl:text>  </xsl:text>
3003 <xsl:text>| </xsl:text>
3006 <xsl:value-of select="./@name"/>
3007 <xsl:text>: </xsl:text>
3008 <xsl:apply-templates select="./*[1]">
3009 <xsl:with-param name="current_indent" select="$current_indent + 2*string-length(./@name) + 5"/>
3010 </xsl:apply-templates>
3018 <xsl:template match="Variable">
3019 <xsl:param name="current_indent" select="0"/>
3021 VARIABLE <xsl:value-of select="@name"/><br/>
3022 TYPE = <xsl:apply-templates select="type/*[1]">
3023 <xsl:with-param name="current_indent" select="$current_indent + 7"/>
3024 </xsl:apply-templates>
3025 <xsl:if test="body">
3027 BODY = <xsl:apply-templates select="body/*[1]">
3028 <xsl:with-param name="current_indent" select="$current_indent + 7"/>
3029 </xsl:apply-templates>
3034 <!--***********************************************************************-->
3036 <!--***********************************************************************-->
3040 <xsl:template match="SECTION">
3041 <xsl:param name="current_indent" select="0"/>
3042 <h1>BEGIN OF SECTION</h1>
3043 <xsl:apply-templates/>
3044 <h1>END OF SECTION</h1>