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

diff --git a/helm/nuprl_stylesheets/nuprl_rules.xsl b/helm/nuprl_stylesheets/nuprl_rules.xsl
deleted file mode 100644
index 6926ddeab..000000000
--- a/helm/nuprl_stylesheets/nuprl_rules.xsl
+++ /dev/null
@@ -1,876 +0,0 @@
-<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
-                              xmlns:m="http://www.w3.org/1998/Math/MathML"
-                              xmlns:cn="http://www.......">
-
-<xsl:template match="level-expression">
-  <m:apply>
-    <m:ci>level-exp</m:ci>
-    <m:ci>
-      <xsl:value-of select="@level"/>
-    </m:ci>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="parameter-substitution-list">
-  <m:apply>
-    <m:ci>parameter-substitution-list</m:ci>
-    <m:ci>
-      <xsl:value-of select="@val"/>
-    </m:ci>
-  </m:apply>
-</xsl:template>
-
-
-<xsl:template match="tag">
-  <m:apply>
-    <m:ci>tag <xsl:value-of select="@step"/>:</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="dependent_functionFormation">
-  <m:apply>
-    <m:ci>dependent_functionFormation</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="independent_functionFormation">
-  <m:ci>independent_functionFormation</m:ci>
-</xsl:template>
-
-<xsl:template match="functionEquality">
-  <m:apply>
-    <m:ci>functionEquality</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="independent_functionEquality">
-  <m:ci>independent_functionEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="lambdaEquality">
-  <m:apply>
-    <m:ci>lambdaEquality</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="lambdaFormation">
-  <m:apply>
-    <m:ci>lambdaFormation</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="applyEquality">
-  <m:apply>
-    <m:ci>applyEquality</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="independent_functionElimination">
-  <m:apply>
-    <m:ci>independent_functionElimination</m:ci>
-    <m:cn>
-      <xsl:value-of select="@number_hyp"/>
-    </m:cn>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="dependent_functionElimination">
-  <m:apply>
-    <m:ci>dependent_functionElimination</m:ci>
-    <m:cn>
-      <xsl:value-of select="@number_hyp"/>
-    </m:cn>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="applyReduce">
-  <m:ci>functionEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="functionExtensionality">
-  <m:apply>
-    <m:ci>functionExtensionality</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="dependent_productFormation">
-  <m:apply>
-    <m:ci>dependent_productFormation</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="independent_productFormation">
-  <m:ci>independent_productFormation</m:ci>
-</xsl:template>
-
-<xsl:template match="productEquality">
-  <m:apply>
-    <m:ci>productEquality</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="independent_productEquality">
-  <m:ci>independent_productEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="dependent_pairEquality">
-  <m:apply>
-    <m:ci>dependent_pairEquality</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="dependent_pairFormation">
-  <m:apply>
-    <m:ci>dependent_pairFormation</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="independent_pairEquality">
-  <m:ci>independent_pairEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="independent_pairFormation">
-  <m:ci>independent_pairFormation</m:ci>
-</xsl:template>
-
-<xsl:template match="spreadEquality">
-  <m:apply>
-    <m:ci>spreadEquality</m:ci>
-    <m:cn>
-      <xsl:value-of select="@number_hyp"/>
-    </m:cn>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="productElimination">
-  <m:apply>
-    <m:ci>productElimination</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="spreadReduce">
-  <m:ci>spreadReduce</m:ci>
-</xsl:template>
-
-<xsl:template match="unionFormation">
-  <m:ci>unionFormation</m:ci>
-</xsl:template>
-
-<xsl:template match="unionEquality"> 
-  <m:ci>unionEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="inlEquality">
-  <m:apply>
-    <m:ci>inlEquality</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="inlFormation">
-  <m:apply>
-    <m:ci>inlFormation</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="inrEquality">
-  <m:apply>
-    <m:ci>inrEquality</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="inrFormation">
-  <m:apply>
-    <m:ci>inrFormation</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="decideEquality">
-  <m:apply>
-    <m:ci>decideEquality</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="unionElimination">
-  <m:apply>
-    <m:ci>unionElimination</m:ci>
-    <m:cn>
-      <xsl:value-of select="@number_hyp"/>
-    </m:cn>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="decideReduceLeft">
-  <m:ci>decideReduceLeft</m:ci>
-</xsl:template>
-
-<xsl:template match="decideReduceRight">
-  <m:ci>decideReduceRight</m:ci>
-</xsl:template>
-
-<xsl:template match="universeFormation">
-  <m:apply>
-    <m:ci>universeFormation</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="universeEquality">
-  <m:ci>universeEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="cumulativity">
-  <m:apply>
-    <m:ci>cumulativity</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="equalityFormation">
-  <m:apply>
-    <m:ci>equalityFormation</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="equalityEquality">
-  <m:ci>equalityEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="axiomEquality">
-  <m:ci>axiomEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="equalityElimination">
-  <m:apply>
-    <m:ci>equalityElimination</m:ci>
-    <m:cn>
-      <xsl:value-of select="@number_hyp"/>
-    </m:cn>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="hypothesisEquality">
-  <m:apply>
-    <m:ci>hypothesisEquality</m:ci>
-    <m:cn>
-      <xsl:value-of select="@number_hyp"/>
-    </m:cn>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="substitution">
-  <m:apply>
-    <m:ci>substitution</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="equality">
-  <m:ci>equality</m:ci>
-</xsl:template>
-
-<xsl:template match="voidFormation">
-  <m:ci>voidFormation</m:ci>
-</xsl:template>
-
-<xsl:template match="voidEquality">
-  <m:ci>voidEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="anyEquality">
-  <m:ci>anyEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="voidElimination">
-  <m:apply>
-    <m:ci>voidElimination</m:ci>
-    <m:cn>
-      <xsl:value-of select="@number_hyp"/>
-    </m:cn>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="atomFormation">
-  <m:ci>atomFormation</m:ci>
-</xsl:template>
-
-<xsl:template match="atomEquality">
-  <m:ci>atomEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="tokenEquality">
-  <m:ci>tokenEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="tokenFormation">
-  <m:apply>
-    <m:ci>tokenFormation</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="atom_eqEquality">
-  <m:apply>
-    <m:ci>atom_eqEquality</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="atom_eqReduceTrue">
-  <m:apply>
-    <m:ci>atom_eqReduceTrue</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="atom_eqReduceFalse">
-  <m:ci>atom_eqReduceFalse</m:ci>
-</xsl:template>
-
-<xsl:template match="intFormation">
-  <m:ci>intFormation</m:ci>
-</xsl:template>
-
-<xsl:template match="intEquality">
-  <m:ci>intEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="natural_numberEquality">
-  <m:ci>natural_numberEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="minusEquality">
-  <m:ci>minusEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="addEquality">
-  <m:ci>addEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="subtractEquality">
-  <m:ci>subtractEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="multiplyEquality">
-  <m:ci>multiplyEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="divideFormation">
-  <m:ci>divideFormation</m:ci>
-</xsl:template>
-
-<xsl:template match="addEquality">
-  <m:ci>addEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="subtractEquality">
-  <m:ci>subtractEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="multiplyEquality">
-  <m:ci>multiplyEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="divideEquality">
-  <m:ci>divideEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="remainderBounds1">
-  <m:ci>remainderBounds1</m:ci>
-</xsl:template>
-
-<xsl:template match="remainderBounds2">
-  <m:ci>remainderBounds2</m:ci>
-</xsl:template>
-
-<xsl:template match="remainderBounds3">
-  <m:ci>remainderBounds3</m:ci>
-</xsl:template>
-
-<xsl:template match="remainderBounds4">
-  <m:ci>remainderBounds4</m:ci>
-</xsl:template>
-
-<xsl:template match="divideRemainderSum">
-  <m:ci>divideRemainderSum</m:ci>
-</xsl:template>
-
-<xsl:template match="arith">
-  <m:apply>
-    <m:ci>arith</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="indEquality">
-  <m:apply>
-    <m:ci>indEquality</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="intElimination">
-  <m:apply>
-    <m:ci>intElimination</m:ci>
-    <m:cn>
-      <xsl:value-of select="@number_hyp"/>
-    </m:cn>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="indReduceDown">
-  <m:ci>indReduceDown</m:ci>
-</xsl:template>
-
-<xsl:template match="indReduceUp">
-  <m:ci>indReduceUp</m:ci>
-</xsl:template>
-
-<xsl:template match="indReduceBase">
-  <m:ci>indReduceBase</m:ci>
-</xsl:template>
-
-<xsl:template match="ind_eqEquality">
-  <m:ci>ind_eqEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="ind_eqReduceTrue">
-  <m:ci>ind_eqReduceTrue</m:ci>
-</xsl:template>
-
-<xsl:template match="ind_eqReduceFalse">
-  <m:ci>ind_eqReduceFalse</m:ci>
-</xsl:template>
-
-<xsl:template match="lessEquality">
-  <m:ci>lessEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="lessReduceTrue">
-  <m:ci>lessReduceTrue</m:ci>
-</xsl:template>
-
-<xsl:template match="lessReduceFalse">
-  <m:ci>lessReduceFalse</m:ci>
-</xsl:template>
-
-<xsl:template match="less_thanEquality">
-  <m:ci>less_thanEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="less_thanFormation">
-  <m:ci>less_thanFormation</m:ci>
-</xsl:template>
-
-<xsl:template match="less_thanMember">
-  <m:ci>less_thanMember</m:ci>
-</xsl:template>
-
-<xsl:template match="listFormation">
-  <m:ci>listFormation</m:ci>
-</xsl:template>
-
-<xsl:template match="listEquality">
-  <m:ci>listEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="nilEquality">
-  <m:apply>
-    <m:ci>nilEquality</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="nilFormation">
-  <m:apply>
-    <m:ci>nilFormation</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="consFormation">
-  <m:ci>consFormation</m:ci>
-</xsl:template>
-
-<xsl:template match="consEquality">
-  <m:ci>consEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="list_indEquality">
-  <m:apply>
-    <m:ci>list_indEquality</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="listElimination">
-  <m:apply>
-    <m:ci>listElimination</m:ci>
-    <m:cn>
-      <xsl:value-of select="@number_hyp"/>
-    </m:cn>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="list_indReduceUp">
-  <m:ci>list_indReduceUp</m:ci>
-</xsl:template>
-
-<xsl:template match="list_indReduceBase">
-  <m:ci>list_indReduceBase</m:ci>
-</xsl:template>
-
-<xsl:template match="recEquality">
-  <m:apply>
-    <m:ci>recEquality</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="rec_memberEquality">
-  <m:apply>
-    <m:ci>rec_memberEquality</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="rec_memberFormation">
-  <m:apply>
-    <m:ci>rec_memberFormation</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="rec_indEquality">
-  <m:apply>
-    <m:ci>rec_indEquality</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="recElimination">
-  <m:apply>
-    <m:ci>recElimination</m:ci>
-    <m:cn>
-      <xsl:value-of select="@number_hyp"/>
-    </m:cn>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="recUnrollElimination">
-  <m:apply>
-    <m:ci>recUnrollElimination</m:ci>
-    <m:cn>
-      <xsl:value-of select="@number_hyp"/>
-    </m:cn>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="dependent_setFormation">
-  <m:apply>
-    <m:ci>dependent_setFormation</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="independent_setFormation">
-  <m:ci>independent_setFormation</m:ci>
-</xsl:template>
-
-<xsl:template match="setEquality">
-  <m:apply>
-    <m:ci>setEquality</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="dependent_set_memberEquality">
-  <m:apply>
-    <m:ci>dependent_set_memberEquality</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="dependent_set_memberFormation">
-  <m:apply>
-    <m:ci>dependent_set_memberFormation</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="independent_set_memberEquality">
-  <m:ci>independent_set_memberEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="independent_set_memberFormation">
-  <m:apply>
-    <m:ci>independent_set_memberFormation</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="setElimination">
-  <m:apply>
-    <m:ci>setElimination</m:ci>
-    <m:cn>
-      <xsl:value-of select="@number_hyp"/>
-    </m:cn>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="isectFormation">
-  <m:apply>
-    <m:ci>isectFormation</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="isectEquality">
-  <m:apply>
-    <m:ci>isectEquality</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="isect_memberEquality">
-  <m:apply>
-    <m:ci>isect_memberEquality</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="isect_memberFormation">
-  <m:apply>
-    <m:ci>isect_memberFormation</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="isect_member_caseEquality">
-  <m:apply>
-    <m:ci>isect_member_caseEquality</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="isectElimination">
-  <m:apply>
-    <m:ci>isectElimination</m:ci>
-    <m:cn>
-      <xsl:value-of select="@number_hyp"/>
-    </m:cn>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="quotientFormation">
-  <m:apply>
-    <m:ci>quotientFormation</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="quotientWeakEquality">
-  <m:apply>
-    <m:ci>quotientWeakEquality</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="quotientEquality">
-  <m:ci>quotientEquality</m:ci>
-</xsl:template>
-
-<xsl:template match="quotient_memberWeakEquality">
-  <m:apply>
-    <m:ci>quotient_memberWeakEquality</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="quotient_memberFormation">
-  <m:apply>
-    <m:ci>quotient_memberFormation</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="quotient_memberEquality">
-  <m:apply>
-    <m:ci>quotient_memberEquality</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="quotient_equalityElimination">
-  <m:apply>
-    <m:ci>quotient_equalityElimination</m:ci>
-    <m:cn>
-      <xsl:value-of select="@number_hyp"/>
-    </m:cn>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="quotientElimination">
-  <m:apply>
-    <m:ci>quotientElimination</m:ci>
-    <m:cn>
-      <xsl:value-of select="@number_hyp"/>
-    </m:cn>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="quotientElimination_2">
-  <m:apply>
-    <m:ci>quotientElimination_2</m:ci>
-    <m:cn> 
-      <xsl:value-of select="@number_hyp"/>
-    </m:cn>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="direct_computation">
-  <m:apply>
-    <m:ci>direct_computation</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="reverse_direct_computation">
-  <m:apply>
-    <m:ci>reverse_direct_computation</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="direct_computation_hypothesis">
-  <m:apply>
-    <m:ci>direct_computation_hypothesis</m:ci>
-    <m:cn>
-      <xsl:value-of select="@number_hyp"/>
-    </m:cn>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="reverse_direct_computation_hypothesis">
-  <m:apply>
-    <m:ci>reverse_direct_computation_hypothesis</m:ci>
-    <m:cn>
-      <xsl:value-of select="@number_hyp"/>
-    </m:cn>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="ruleinstance/hypothesis">
-  <m:apply>
-    <m:ci>hypothesis</m:ci>
-    <m:cn>
-      <xsl:value-of select="@number_hyp"/>
-    </m:cn>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="thin">
-  <m:apply>
-    <m:ci>thin</m:ci>
-    <m:cn>
-      <xsl:value-of select="@number_hyp"/>
-    </m:cn>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="cut">
-  <m:apply>
-    <m:ci>cut</m:ci>
-    <m:cn>
-      <xsl:value-of select="@number_hyp"/>
-    </m:cn>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="hyp_replacement">
-  <m:apply>
-    <m:ci>hyp_replacement</m:ci>
-    <m:cn>
-      <xsl:value-of select="@number_hyp"/>
-    </m:cn>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="lemma">
-  <m:apply>
-    <m:ci>lemma</m:ci>
-    <m:ci>
-      <xsl:value-of select="@name"/>
-    </m:ci>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="extract">
-  <m:apply>
-    <m:ci>extract</m:ci>
-    <m:ci>
-      <xsl:value-of select="@name"/>
-    </m:ci>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="instantiate">
-  <m:apply>
-    <m:ci>instantiate</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="because">
-  <m:ci>because</m:ci>
-</xsl:template>
-
-<xsl:template match="rename">
-  <m:apply>
-    <m:ci>rename</m:ci>
-    <xsl:apply-templates/>
-  </m:apply>
-</xsl:template>
-
-<xsl:template match="introduction">
-  <m:apply>
-    <m:ci>introducition</m:ci>
-    <xsl:apply-templates/> 
-  </m:apply>
-</xsl:template>
-
-</xsl:stylesheet>