]> matita.cs.unibo.it Git - helm.git/blob - helm/nuprl_stylesheets/nuprl_proof.xsl
ocaml 3.09 transition
[helm.git] / helm / nuprl_stylesheets / nuprl_proof.xsl
1 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
2                               xmlns:m="http://www.w3.org/1998/Math/MathML"
3                               xmlns:cn="http://www.......">
4
5
6 <xsl:template match="NuPrlProof">
7   <Definition>
8     <Params />
9     <body>
10       <xsl:apply-templates/>
11     </body>
12     <type>
13       <xsl:apply-templates select="node/sequent/conclusion/*[1]"/>
14     </type>
15   </Definition>
16 </xsl:template>
17
18 <xsl:template match="NuPrlDefinition">
19  <NuPrlDefinition>
20   <xsl:apply-templates select="*"/>
21  </NuPrlDefinition>
22 </xsl:template>
23
24 <xsl:template match="node">
25   <xsl:element name="Node">
26     <xsl:apply-templates/>
27   </xsl:element>
28 </xsl:template>
29
30 <xsl:template match="sequent">
31   <xsl:element name="Sequent">
32     <xsl:attribute name="id">
33       <xsl:value-of select="@number"/>
34     </xsl:attribute>
35     <xsl:apply-templates/>
36   </xsl:element>
37 </xsl:template>
38
39 <xsl:template match="hypothesis">
40   <xsl:element name="Decl">
41     <xsl:if test="@var!=&quot;&quot;">
42       <xsl:attribute name="name">
43         <xsl:value-of select="@var"/>
44       </xsl:attribute>
45     </xsl:if>
46     <xsl:apply-templates/>
47   </xsl:element>
48 </xsl:template>
49
50 <xsl:template match="conclusion">
51   <xsl:element name="Goal">
52     <xsl:apply-templates/>
53   </xsl:element>
54 </xsl:template>
55
56 <xsl:template match="ruleinstance">
57   <xsl:element name="Rule">
58     <xsl:apply-templates/>
59   </xsl:element>
60 </xsl:template>
61
62 <xsl:template match="tacticinstance">
63   <TacticInstance name="{@name}" uri="{@uri}"/>
64 </xsl:template>
65
66 <xsl:template match="tacticproof">
67   <xsl:element name="TacticProof">
68     <xsl:apply-templates/>
69   </xsl:element>
70 </xsl:template>
71
72 </xsl:stylesheet>