]> matita.cs.unibo.it Git - helm.git/blob - helm/nuprl_stylesheets/nuprl_rules.xsl
use a dummy location when no location is provided
[helm.git] / helm / nuprl_stylesheets / nuprl_rules.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 <xsl:template match="level-expression">
6   <m:apply>
7     <m:ci>level-exp</m:ci>
8     <m:ci>
9       <xsl:value-of select="@level"/>
10     </m:ci>
11   </m:apply>
12 </xsl:template>
13
14 <xsl:template match="parameter-substitution-list">
15   <m:apply>
16     <m:ci>parameter-substitution-list</m:ci>
17     <m:ci>
18       <xsl:value-of select="@val"/>
19     </m:ci>
20   </m:apply>
21 </xsl:template>
22
23
24 <xsl:template match="tag">
25   <m:apply>
26     <m:ci>tag <xsl:value-of select="@step"/>:</m:ci>
27     <xsl:apply-templates/>
28   </m:apply>
29 </xsl:template>
30
31 <xsl:template match="dependent_functionFormation">
32   <m:apply>
33     <m:ci>dependent_functionFormation</m:ci>
34     <xsl:apply-templates/>
35   </m:apply>
36 </xsl:template>
37
38 <xsl:template match="independent_functionFormation">
39   <m:ci>independent_functionFormation</m:ci>
40 </xsl:template>
41
42 <xsl:template match="functionEquality">
43   <m:apply>
44     <m:ci>functionEquality</m:ci>
45     <xsl:apply-templates/>
46   </m:apply>
47 </xsl:template>
48
49 <xsl:template match="independent_functionEquality">
50   <m:ci>independent_functionEquality</m:ci>
51 </xsl:template>
52
53 <xsl:template match="lambdaEquality">
54   <m:apply>
55     <m:ci>lambdaEquality</m:ci>
56     <xsl:apply-templates/>
57   </m:apply>
58 </xsl:template>
59
60 <xsl:template match="lambdaFormation">
61   <m:apply>
62     <m:ci>lambdaFormation</m:ci>
63     <xsl:apply-templates/>
64   </m:apply>
65 </xsl:template>
66
67 <xsl:template match="applyEquality">
68   <m:apply>
69     <m:ci>applyEquality</m:ci>
70     <xsl:apply-templates/>
71   </m:apply>
72 </xsl:template>
73
74 <xsl:template match="independent_functionElimination">
75   <m:apply>
76     <m:ci>independent_functionElimination</m:ci>
77     <m:cn>
78       <xsl:value-of select="@number_hyp"/>
79     </m:cn>
80     <xsl:apply-templates/>
81   </m:apply>
82 </xsl:template>
83
84 <xsl:template match="dependent_functionElimination">
85   <m:apply>
86     <m:ci>dependent_functionElimination</m:ci>
87     <m:cn>
88       <xsl:value-of select="@number_hyp"/>
89     </m:cn>
90     <xsl:apply-templates/>
91   </m:apply>
92 </xsl:template>
93
94 <xsl:template match="applyReduce">
95   <m:ci>functionEquality</m:ci>
96 </xsl:template>
97
98 <xsl:template match="functionExtensionality">
99   <m:apply>
100     <m:ci>functionExtensionality</m:ci>
101     <xsl:apply-templates/>
102   </m:apply>
103 </xsl:template>
104
105 <xsl:template match="dependent_productFormation">
106   <m:apply>
107     <m:ci>dependent_productFormation</m:ci>
108     <xsl:apply-templates/>
109   </m:apply>
110 </xsl:template>
111
112 <xsl:template match="independent_productFormation">
113   <m:ci>independent_productFormation</m:ci>
114 </xsl:template>
115
116 <xsl:template match="productEquality">
117   <m:apply>
118     <m:ci>productEquality</m:ci>
119     <xsl:apply-templates/>
120   </m:apply>
121 </xsl:template>
122
123 <xsl:template match="independent_productEquality">
124   <m:ci>independent_productEquality</m:ci>
125 </xsl:template>
126
127 <xsl:template match="dependent_pairEquality">
128   <m:apply>
129     <m:ci>dependent_pairEquality</m:ci>
130     <xsl:apply-templates/>
131   </m:apply>
132 </xsl:template>
133
134 <xsl:template match="dependent_pairFormation">
135   <m:apply>
136     <m:ci>dependent_pairFormation</m:ci>
137     <xsl:apply-templates/>
138   </m:apply>
139 </xsl:template>
140
141 <xsl:template match="independent_pairEquality">
142   <m:ci>independent_pairEquality</m:ci>
143 </xsl:template>
144
145 <xsl:template match="independent_pairFormation">
146   <m:ci>independent_pairFormation</m:ci>
147 </xsl:template>
148
149 <xsl:template match="spreadEquality">
150   <m:apply>
151     <m:ci>spreadEquality</m:ci>
152     <m:cn>
153       <xsl:value-of select="@number_hyp"/>
154     </m:cn>
155     <xsl:apply-templates/>
156   </m:apply>
157 </xsl:template>
158
159 <xsl:template match="productElimination">
160   <m:apply>
161     <m:ci>productElimination</m:ci>
162     <xsl:apply-templates/>
163   </m:apply>
164 </xsl:template>
165
166 <xsl:template match="spreadReduce">
167   <m:ci>spreadReduce</m:ci>
168 </xsl:template>
169
170 <xsl:template match="unionFormation">
171   <m:ci>unionFormation</m:ci>
172 </xsl:template>
173
174 <xsl:template match="unionEquality"> 
175   <m:ci>unionEquality</m:ci>
176 </xsl:template>
177
178 <xsl:template match="inlEquality">
179   <m:apply>
180     <m:ci>inlEquality</m:ci>
181     <xsl:apply-templates/>
182   </m:apply>
183 </xsl:template>
184
185 <xsl:template match="inlFormation">
186   <m:apply>
187     <m:ci>inlFormation</m:ci>
188     <xsl:apply-templates/>
189   </m:apply>
190 </xsl:template>
191
192 <xsl:template match="inrEquality">
193   <m:apply>
194     <m:ci>inrEquality</m:ci>
195     <xsl:apply-templates/>
196   </m:apply>
197 </xsl:template>
198
199 <xsl:template match="inrFormation">
200   <m:apply>
201     <m:ci>inrFormation</m:ci>
202     <xsl:apply-templates/>
203   </m:apply>
204 </xsl:template>
205
206 <xsl:template match="decideEquality">
207   <m:apply>
208     <m:ci>decideEquality</m:ci>
209     <xsl:apply-templates/>
210   </m:apply>
211 </xsl:template>
212
213 <xsl:template match="unionElimination">
214   <m:apply>
215     <m:ci>unionElimination</m:ci>
216     <m:cn>
217       <xsl:value-of select="@number_hyp"/>
218     </m:cn>
219     <xsl:apply-templates/>
220   </m:apply>
221 </xsl:template>
222
223 <xsl:template match="decideReduceLeft">
224   <m:ci>decideReduceLeft</m:ci>
225 </xsl:template>
226
227 <xsl:template match="decideReduceRight">
228   <m:ci>decideReduceRight</m:ci>
229 </xsl:template>
230
231 <xsl:template match="universeFormation">
232   <m:apply>
233     <m:ci>universeFormation</m:ci>
234     <xsl:apply-templates/>
235   </m:apply>
236 </xsl:template>
237
238 <xsl:template match="universeEquality">
239   <m:ci>universeEquality</m:ci>
240 </xsl:template>
241
242 <xsl:template match="cumulativity">
243   <m:apply>
244     <m:ci>cumulativity</m:ci>
245     <xsl:apply-templates/>
246   </m:apply>
247 </xsl:template>
248
249 <xsl:template match="equalityFormation">
250   <m:apply>
251     <m:ci>equalityFormation</m:ci>
252     <xsl:apply-templates/>
253   </m:apply>
254 </xsl:template>
255
256 <xsl:template match="equalityEquality">
257   <m:ci>equalityEquality</m:ci>
258 </xsl:template>
259
260 <xsl:template match="axiomEquality">
261   <m:ci>axiomEquality</m:ci>
262 </xsl:template>
263
264 <xsl:template match="equalityElimination">
265   <m:apply>
266     <m:ci>equalityElimination</m:ci>
267     <m:cn>
268       <xsl:value-of select="@number_hyp"/>
269     </m:cn>
270   </m:apply>
271 </xsl:template>
272
273 <xsl:template match="hypothesisEquality">
274   <m:apply>
275     <m:ci>hypothesisEquality</m:ci>
276     <m:cn>
277       <xsl:value-of select="@number_hyp"/>
278     </m:cn>
279   </m:apply>
280 </xsl:template>
281
282 <xsl:template match="substitution">
283   <m:apply>
284     <m:ci>substitution</m:ci>
285     <xsl:apply-templates/>
286   </m:apply>
287 </xsl:template>
288
289 <xsl:template match="equality">
290   <m:ci>equality</m:ci>
291 </xsl:template>
292
293 <xsl:template match="voidFormation">
294   <m:ci>voidFormation</m:ci>
295 </xsl:template>
296
297 <xsl:template match="voidEquality">
298   <m:ci>voidEquality</m:ci>
299 </xsl:template>
300
301 <xsl:template match="anyEquality">
302   <m:ci>anyEquality</m:ci>
303 </xsl:template>
304
305 <xsl:template match="voidElimination">
306   <m:apply>
307     <m:ci>voidElimination</m:ci>
308     <m:cn>
309       <xsl:value-of select="@number_hyp"/>
310     </m:cn>
311   </m:apply>
312 </xsl:template>
313
314 <xsl:template match="atomFormation">
315   <m:ci>atomFormation</m:ci>
316 </xsl:template>
317
318 <xsl:template match="atomEquality">
319   <m:ci>atomEquality</m:ci>
320 </xsl:template>
321
322 <xsl:template match="tokenEquality">
323   <m:ci>tokenEquality</m:ci>
324 </xsl:template>
325
326 <xsl:template match="tokenFormation">
327   <m:apply>
328     <m:ci>tokenFormation</m:ci>
329     <xsl:apply-templates/>
330   </m:apply>
331 </xsl:template>
332
333 <xsl:template match="atom_eqEquality">
334   <m:apply>
335     <m:ci>atom_eqEquality</m:ci>
336     <xsl:apply-templates/>
337   </m:apply>
338 </xsl:template>
339
340 <xsl:template match="atom_eqReduceTrue">
341   <m:apply>
342     <m:ci>atom_eqReduceTrue</m:ci>
343     <xsl:apply-templates/>
344   </m:apply>
345 </xsl:template>
346
347 <xsl:template match="atom_eqReduceFalse">
348   <m:ci>atom_eqReduceFalse</m:ci>
349 </xsl:template>
350
351 <xsl:template match="intFormation">
352   <m:ci>intFormation</m:ci>
353 </xsl:template>
354
355 <xsl:template match="intEquality">
356   <m:ci>intEquality</m:ci>
357 </xsl:template>
358
359 <xsl:template match="natural_numberEquality">
360   <m:ci>natural_numberEquality</m:ci>
361 </xsl:template>
362
363 <xsl:template match="minusEquality">
364   <m:ci>minusEquality</m:ci>
365 </xsl:template>
366
367 <xsl:template match="addEquality">
368   <m:ci>addEquality</m:ci>
369 </xsl:template>
370
371 <xsl:template match="subtractEquality">
372   <m:ci>subtractEquality</m:ci>
373 </xsl:template>
374
375 <xsl:template match="multiplyEquality">
376   <m:ci>multiplyEquality</m:ci>
377 </xsl:template>
378
379 <xsl:template match="divideFormation">
380   <m:ci>divideFormation</m:ci>
381 </xsl:template>
382
383 <xsl:template match="addEquality">
384   <m:ci>addEquality</m:ci>
385 </xsl:template>
386
387 <xsl:template match="subtractEquality">
388   <m:ci>subtractEquality</m:ci>
389 </xsl:template>
390
391 <xsl:template match="multiplyEquality">
392   <m:ci>multiplyEquality</m:ci>
393 </xsl:template>
394
395 <xsl:template match="divideEquality">
396   <m:ci>divideEquality</m:ci>
397 </xsl:template>
398
399 <xsl:template match="remainderBounds1">
400   <m:ci>remainderBounds1</m:ci>
401 </xsl:template>
402
403 <xsl:template match="remainderBounds2">
404   <m:ci>remainderBounds2</m:ci>
405 </xsl:template>
406
407 <xsl:template match="remainderBounds3">
408   <m:ci>remainderBounds3</m:ci>
409 </xsl:template>
410
411 <xsl:template match="remainderBounds4">
412   <m:ci>remainderBounds4</m:ci>
413 </xsl:template>
414
415 <xsl:template match="divideRemainderSum">
416   <m:ci>divideRemainderSum</m:ci>
417 </xsl:template>
418
419 <xsl:template match="arith">
420   <m:apply>
421     <m:ci>arith</m:ci>
422     <xsl:apply-templates/>
423   </m:apply>
424 </xsl:template>
425
426 <xsl:template match="indEquality">
427   <m:apply>
428     <m:ci>indEquality</m:ci>
429     <xsl:apply-templates/>
430   </m:apply>
431 </xsl:template>
432
433 <xsl:template match="intElimination">
434   <m:apply>
435     <m:ci>intElimination</m:ci>
436     <m:cn>
437       <xsl:value-of select="@number_hyp"/>
438     </m:cn>
439     <xsl:apply-templates/>
440   </m:apply>
441 </xsl:template>
442
443 <xsl:template match="indReduceDown">
444   <m:ci>indReduceDown</m:ci>
445 </xsl:template>
446
447 <xsl:template match="indReduceUp">
448   <m:ci>indReduceUp</m:ci>
449 </xsl:template>
450
451 <xsl:template match="indReduceBase">
452   <m:ci>indReduceBase</m:ci>
453 </xsl:template>
454
455 <xsl:template match="ind_eqEquality">
456   <m:ci>ind_eqEquality</m:ci>
457 </xsl:template>
458
459 <xsl:template match="ind_eqReduceTrue">
460   <m:ci>ind_eqReduceTrue</m:ci>
461 </xsl:template>
462
463 <xsl:template match="ind_eqReduceFalse">
464   <m:ci>ind_eqReduceFalse</m:ci>
465 </xsl:template>
466
467 <xsl:template match="lessEquality">
468   <m:ci>lessEquality</m:ci>
469 </xsl:template>
470
471 <xsl:template match="lessReduceTrue">
472   <m:ci>lessReduceTrue</m:ci>
473 </xsl:template>
474
475 <xsl:template match="lessReduceFalse">
476   <m:ci>lessReduceFalse</m:ci>
477 </xsl:template>
478
479 <xsl:template match="less_thanEquality">
480   <m:ci>less_thanEquality</m:ci>
481 </xsl:template>
482
483 <xsl:template match="less_thanFormation">
484   <m:ci>less_thanFormation</m:ci>
485 </xsl:template>
486
487 <xsl:template match="less_thanMember">
488   <m:ci>less_thanMember</m:ci>
489 </xsl:template>
490
491 <xsl:template match="listFormation">
492   <m:ci>listFormation</m:ci>
493 </xsl:template>
494
495 <xsl:template match="listEquality">
496   <m:ci>listEquality</m:ci>
497 </xsl:template>
498
499 <xsl:template match="nilEquality">
500   <m:apply>
501     <m:ci>nilEquality</m:ci>
502     <xsl:apply-templates/>
503   </m:apply>
504 </xsl:template>
505
506 <xsl:template match="nilFormation">
507   <m:apply>
508     <m:ci>nilFormation</m:ci>
509     <xsl:apply-templates/>
510   </m:apply>
511 </xsl:template>
512
513 <xsl:template match="consFormation">
514   <m:ci>consFormation</m:ci>
515 </xsl:template>
516
517 <xsl:template match="consEquality">
518   <m:ci>consEquality</m:ci>
519 </xsl:template>
520
521 <xsl:template match="list_indEquality">
522   <m:apply>
523     <m:ci>list_indEquality</m:ci>
524     <xsl:apply-templates/>
525   </m:apply>
526 </xsl:template>
527
528 <xsl:template match="listElimination">
529   <m:apply>
530     <m:ci>listElimination</m:ci>
531     <m:cn>
532       <xsl:value-of select="@number_hyp"/>
533     </m:cn>
534     <xsl:apply-templates/>
535   </m:apply>
536 </xsl:template>
537
538 <xsl:template match="list_indReduceUp">
539   <m:ci>list_indReduceUp</m:ci>
540 </xsl:template>
541
542 <xsl:template match="list_indReduceBase">
543   <m:ci>list_indReduceBase</m:ci>
544 </xsl:template>
545
546 <xsl:template match="recEquality">
547   <m:apply>
548     <m:ci>recEquality</m:ci>
549     <xsl:apply-templates/>
550   </m:apply>
551 </xsl:template>
552
553 <xsl:template match="rec_memberEquality">
554   <m:apply>
555     <m:ci>rec_memberEquality</m:ci>
556     <xsl:apply-templates/>
557   </m:apply>
558 </xsl:template>
559
560 <xsl:template match="rec_memberFormation">
561   <m:apply>
562     <m:ci>rec_memberFormation</m:ci>
563     <xsl:apply-templates/>
564   </m:apply>
565 </xsl:template>
566
567 <xsl:template match="rec_indEquality">
568   <m:apply>
569     <m:ci>rec_indEquality</m:ci>
570     <xsl:apply-templates/>
571   </m:apply>
572 </xsl:template>
573
574 <xsl:template match="recElimination">
575   <m:apply>
576     <m:ci>recElimination</m:ci>
577     <m:cn>
578       <xsl:value-of select="@number_hyp"/>
579     </m:cn>
580     <xsl:apply-templates/>
581   </m:apply>
582 </xsl:template>
583
584 <xsl:template match="recUnrollElimination">
585   <m:apply>
586     <m:ci>recUnrollElimination</m:ci>
587     <m:cn>
588       <xsl:value-of select="@number_hyp"/>
589     </m:cn>
590     <xsl:apply-templates/>
591   </m:apply>
592 </xsl:template>
593
594 <xsl:template match="dependent_setFormation">
595   <m:apply>
596     <m:ci>dependent_setFormation</m:ci>
597     <xsl:apply-templates/>
598   </m:apply>
599 </xsl:template>
600
601 <xsl:template match="independent_setFormation">
602   <m:ci>independent_setFormation</m:ci>
603 </xsl:template>
604
605 <xsl:template match="setEquality">
606   <m:apply>
607     <m:ci>setEquality</m:ci>
608     <xsl:apply-templates/>
609   </m:apply>
610 </xsl:template>
611
612 <xsl:template match="dependent_set_memberEquality">
613   <m:apply>
614     <m:ci>dependent_set_memberEquality</m:ci>
615     <xsl:apply-templates/>
616   </m:apply>
617 </xsl:template>
618
619 <xsl:template match="dependent_set_memberFormation">
620   <m:apply>
621     <m:ci>dependent_set_memberFormation</m:ci>
622     <xsl:apply-templates/>
623   </m:apply>
624 </xsl:template>
625
626 <xsl:template match="independent_set_memberEquality">
627   <m:ci>independent_set_memberEquality</m:ci>
628 </xsl:template>
629
630 <xsl:template match="independent_set_memberFormation">
631   <m:apply>
632     <m:ci>independent_set_memberFormation</m:ci>
633     <xsl:apply-templates/>
634   </m:apply>
635 </xsl:template>
636
637 <xsl:template match="setElimination">
638   <m:apply>
639     <m:ci>setElimination</m:ci>
640     <m:cn>
641       <xsl:value-of select="@number_hyp"/>
642     </m:cn>
643     <xsl:apply-templates/>
644   </m:apply>
645 </xsl:template>
646
647 <xsl:template match="isectFormation">
648   <m:apply>
649     <m:ci>isectFormation</m:ci>
650     <xsl:apply-templates/>
651   </m:apply>
652 </xsl:template>
653
654 <xsl:template match="isectEquality">
655   <m:apply>
656     <m:ci>isectEquality</m:ci>
657     <xsl:apply-templates/>
658   </m:apply>
659 </xsl:template>
660
661 <xsl:template match="isect_memberEquality">
662   <m:apply>
663     <m:ci>isect_memberEquality</m:ci>
664     <xsl:apply-templates/>
665   </m:apply>
666 </xsl:template>
667
668 <xsl:template match="isect_memberFormation">
669   <m:apply>
670     <m:ci>isect_memberFormation</m:ci>
671     <xsl:apply-templates/>
672   </m:apply>
673 </xsl:template>
674
675 <xsl:template match="isect_member_caseEquality">
676   <m:apply>
677     <m:ci>isect_member_caseEquality</m:ci>
678     <xsl:apply-templates/>
679   </m:apply>
680 </xsl:template>
681
682 <xsl:template match="isectElimination">
683   <m:apply>
684     <m:ci>isectElimination</m:ci>
685     <m:cn>
686       <xsl:value-of select="@number_hyp"/>
687     </m:cn>
688     <xsl:apply-templates/>
689   </m:apply>
690 </xsl:template>
691
692 <xsl:template match="quotientFormation">
693   <m:apply>
694     <m:ci>quotientFormation</m:ci>
695     <xsl:apply-templates/>
696   </m:apply>
697 </xsl:template>
698
699 <xsl:template match="quotientWeakEquality">
700   <m:apply>
701     <m:ci>quotientWeakEquality</m:ci>
702     <xsl:apply-templates/>
703   </m:apply>
704 </xsl:template>
705
706 <xsl:template match="quotientEquality">
707   <m:ci>quotientEquality</m:ci>
708 </xsl:template>
709
710 <xsl:template match="quotient_memberWeakEquality">
711   <m:apply>
712     <m:ci>quotient_memberWeakEquality</m:ci>
713     <xsl:apply-templates/>
714   </m:apply>
715 </xsl:template>
716
717 <xsl:template match="quotient_memberFormation">
718   <m:apply>
719     <m:ci>quotient_memberFormation</m:ci>
720     <xsl:apply-templates/>
721   </m:apply>
722 </xsl:template>
723
724 <xsl:template match="quotient_memberEquality">
725   <m:apply>
726     <m:ci>quotient_memberEquality</m:ci>
727     <xsl:apply-templates/>
728   </m:apply>
729 </xsl:template>
730
731 <xsl:template match="quotient_equalityElimination">
732   <m:apply>
733     <m:ci>quotient_equalityElimination</m:ci>
734     <m:cn>
735       <xsl:value-of select="@number_hyp"/>
736     </m:cn>
737     <xsl:apply-templates/>
738   </m:apply>
739 </xsl:template>
740
741 <xsl:template match="quotientElimination">
742   <m:apply>
743     <m:ci>quotientElimination</m:ci>
744     <m:cn>
745       <xsl:value-of select="@number_hyp"/>
746     </m:cn>
747     <xsl:apply-templates/>
748   </m:apply>
749 </xsl:template>
750
751 <xsl:template match="quotientElimination_2">
752   <m:apply>
753     <m:ci>quotientElimination_2</m:ci>
754     <m:cn> 
755       <xsl:value-of select="@number_hyp"/>
756     </m:cn>
757     <xsl:apply-templates/>
758   </m:apply>
759 </xsl:template>
760
761 <xsl:template match="direct_computation">
762   <m:apply>
763     <m:ci>direct_computation</m:ci>
764     <xsl:apply-templates/>
765   </m:apply>
766 </xsl:template>
767
768 <xsl:template match="reverse_direct_computation">
769   <m:apply>
770     <m:ci>reverse_direct_computation</m:ci>
771     <xsl:apply-templates/>
772   </m:apply>
773 </xsl:template>
774
775 <xsl:template match="direct_computation_hypothesis">
776   <m:apply>
777     <m:ci>direct_computation_hypothesis</m:ci>
778     <m:cn>
779       <xsl:value-of select="@number_hyp"/>
780     </m:cn>
781     <xsl:apply-templates/>
782   </m:apply>
783 </xsl:template>
784
785 <xsl:template match="reverse_direct_computation_hypothesis">
786   <m:apply>
787     <m:ci>reverse_direct_computation_hypothesis</m:ci>
788     <m:cn>
789       <xsl:value-of select="@number_hyp"/>
790     </m:cn>
791     <xsl:apply-templates/>
792   </m:apply>
793 </xsl:template>
794
795 <xsl:template match="ruleinstance/hypothesis">
796   <m:apply>
797     <m:ci>hypothesis</m:ci>
798     <m:cn>
799       <xsl:value-of select="@number_hyp"/>
800     </m:cn>
801   </m:apply>
802 </xsl:template>
803
804 <xsl:template match="thin">
805   <m:apply>
806     <m:ci>thin</m:ci>
807     <m:cn>
808       <xsl:value-of select="@number_hyp"/>
809     </m:cn>
810   </m:apply>
811 </xsl:template>
812
813 <xsl:template match="cut">
814   <m:apply>
815     <m:ci>cut</m:ci>
816     <m:cn>
817       <xsl:value-of select="@number_hyp"/>
818     </m:cn>
819     <xsl:apply-templates/>
820   </m:apply>
821 </xsl:template>
822
823 <xsl:template match="hyp_replacement">
824   <m:apply>
825     <m:ci>hyp_replacement</m:ci>
826     <m:cn>
827       <xsl:value-of select="@number_hyp"/>
828     </m:cn>
829     <xsl:apply-templates/>
830   </m:apply>
831 </xsl:template>
832
833 <xsl:template match="lemma">
834   <m:apply>
835     <m:ci>lemma</m:ci>
836     <m:ci>
837       <xsl:value-of select="@name"/>
838     </m:ci>
839   </m:apply>
840 </xsl:template>
841
842 <xsl:template match="extract">
843   <m:apply>
844     <m:ci>extract</m:ci>
845     <m:ci>
846       <xsl:value-of select="@name"/>
847     </m:ci>
848   </m:apply>
849 </xsl:template>
850
851 <xsl:template match="instantiate">
852   <m:apply>
853     <m:ci>instantiate</m:ci>
854     <xsl:apply-templates/>
855   </m:apply>
856 </xsl:template>
857
858 <xsl:template match="because">
859   <m:ci>because</m:ci>
860 </xsl:template>
861
862 <xsl:template match="rename">
863   <m:apply>
864     <m:ci>rename</m:ci>
865     <xsl:apply-templates/>
866   </m:apply>
867 </xsl:template>
868
869 <xsl:template match="introduction">
870   <m:apply>
871     <m:ci>introducition</m:ci>
872     <xsl:apply-templates/> 
873   </m:apply>
874 </xsl:template>
875
876 </xsl:stylesheet>