X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Flambda.xsl;fp=helm%2Fstyle%2Flambda.xsl;h=0000000000000000000000000000000000000000;hb=bb2953675ebb08267186029b18bc3fdca9c137df;hp=28c876fa07cc55716f8da82a9ad3144c31892001;hpb=1cfcea66d7394a785ec439cd6b03497b276918c4;p=helm.git

diff --git a/helm/style/lambda.xsl b/helm/style/lambda.xsl
deleted file mode 100644
index 28c876fa0..000000000
--- a/helm/style/lambda.xsl
+++ /dev/null
@@ -1,158 +0,0 @@
-<?xml version="1.0"?>
-<!-- Copyright (C) 2000, HELM Team                                     -->
-<!--                                                                   -->
-<!-- This file is part of HELM, an Hypertextual, Electronic            -->
-<!-- Library of Mathematics, developed at the Computer Science         -->
-<!-- Department, University of Bologna, Italy.                         -->
-<!--                                                                   -->
-<!-- HELM is free software; you can redistribute it and/or             -->
-<!-- modify it under the terms of the GNU General Public License       -->
-<!-- as published by the Free Software Foundation; either version 2    -->
-<!-- of the License, or (at your option) any later version.            -->
-<!--                                                                   -->
-<!-- HELM is distributed in the hope that it will be useful,           -->
-<!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
-<!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
-<!-- GNU General Public License for more details.                      -->
-<!--                                                                   -->
-<!-- You should have received a copy of the GNU General Public License -->
-<!-- along with HELM; if not, write to the Free Software               -->
-<!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
-<!-- MA  02111-1307, USA.                                              -->
-<!--                                                                   -->
-<!-- For details, see the HELM World-Wide-Web page,                    -->
-<!-- http://cs.unibo.it/helm/.                                         -->
-
-<!--******************************************************************--> 
-<!-- Lambda Calculus                                                  -->
-<!-- First draft: March 20 2001, Andrea Asperti                       -->
-<!--******************************************************************-->
-
-<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
-                              xmlns:m="http://www.w3.org/1998/Math/MathML"
-                              xmlns:helm="http://www.cs.unibo.it/helm">
-
-<!-- ************************** LAMBDA ****************************** -->
-
-<!-- subst -->
-<xsl:template match="APPLY[CONST[(attribute::uri='cic:/Rocq/LAMBDA/Terms/subst_rec.con' or attribute::uri='cic:/Rocq/LAMBDA/Substitution/subst_rec_r.con')] and count(child::*) = 4]" mode="pure">
-	<m:apply>
-         <m:csymbol definitionURL="{CONST/@uri}">subst</m:csymbol>
-         <xsl:apply-templates select="*[3]" mode="pure"/>
-         <xsl:apply-templates select="*[2]" mode="pure"/>
-         <xsl:apply-templates select="*[4]" mode="pure"/>
-        </m:apply>
-</xsl:template>
-
-<xsl:template match="APPLY[CONST[(attribute::uri='cic:/Rocq/LAMBDA/Terms/subst.con' or attribute::uri='cic:/Rocq/LAMBDA/Substitution/subst_r.con')] and count(child::*) = 3]" mode="pure">
-	<m:apply>
-         <m:csymbol definitionURL="{CONST/@uri}">subst</m:csymbol>
-         <xsl:apply-templates select="*[2]" mode="pure"/>
-         <xsl:apply-templates select="*[3]" mode="pure"/>
-         <m:ci>0</m:ci>
-        </m:apply>
-</xsl:template>
-
-<!-- lift -->
-<xsl:template match="APPLY[CONST[(attribute::uri='cic:/Rocq/LAMBDA/Terms/lift_rec.con' or attribute::uri='cic:/Rocq/LAMBDA/Substitution/lift_rec_r.con')] and count(child::*) = 4]" mode="pure">
-	<m:apply>
-         <m:csymbol definitionURL="{CONST/@uri}">lift_with_base</m:csymbol>
-         <xsl:apply-templates select="*[2]" mode="pure"/>
-         <xsl:apply-templates select="*[3]" mode="pure"/>
-         <xsl:apply-templates select="*[4]" mode="pure"/>
-        </m:apply>
-</xsl:template>
-
-<xsl:template match="APPLY[CONST[(attribute::uri='cic:/Rocq/LAMBDA/Terms/lift.con' or attribute::uri='cic:/Rocq/LAMBDA/Substitution/lift_r.con')] and count(child::*) = 3]" mode="pure">
-	<m:apply>
-         <m:csymbol definitionURL="{CONST/@uri}">lift</m:csymbol>
-         <xsl:apply-templates select="*[2]" mode="pure"/>
-         <xsl:apply-templates select="*[3]" mode="pure"/>
-        </m:apply>
-</xsl:template>
-
-<!-- reduction -->
-<xsl:template match="APPLY[MUTIND[(position()='1' and attribute::uri='cic:/Rocq/LAMBDA/Reduction/red1.ind')] and count(child::*) = 3]" mode="pure">
-	<m:apply>
-         <m:csymbol definitionURL="{MUTIND/@uri}">beta_red1</m:csymbol>
-         <xsl:apply-templates select="*[2]" mode="pure"/>
-         <xsl:apply-templates select="*[3]" mode="pure"/>
-        </m:apply>
-</xsl:template>
-
-<xsl:template match="APPLY[MUTIND[(position()='1' and attribute::uri='cic:/Rocq/LAMBDA/Reduction/red.ind')] and count(child::*) = 3]" mode="pure">
-	<m:apply>
-         <m:csymbol definitionURL="{MUTIND/@uri}">beta_red</m:csymbol>
-         <xsl:apply-templates select="*[2]" mode="pure"/>
-         <xsl:apply-templates select="*[3]" mode="pure"/>
-        </m:apply>
-</xsl:template>
-
-<xsl:template match="APPLY[MUTIND[(position()='1' and attribute::uri='cic:/Rocq/LAMBDA/Reduction/par_red1.ind')] and count(child::*) = 3]" mode="pure">
-	<m:apply>
-         <m:csymbol definitionURL="{MUTIND/@uri}">par_beta_red1</m:csymbol>
-         <xsl:apply-templates select="*[2]" mode="pure"/>
-         <xsl:apply-templates select="*[3]" mode="pure"/>
-        </m:apply>
-</xsl:template>
-
-<xsl:template match="APPLY[MUTIND[(position()='1' and attribute::uri='cic:/Rocq/LAMBDA/Reduction/par_red.ind')] and count(child::*) = 3]" mode="pure">
-	<m:apply>
-         <m:csymbol definitionURL="{MUTIND/@uri}">par_beta_red</m:csymbol>
-         <xsl:apply-templates select="*[2]" mode="pure"/>
-         <xsl:apply-templates select="*[3]" mode="pure"/>
-        </m:apply>
-</xsl:template>
-
-<!-- unmark -->
-
-<xsl:template match="APPLY[CONST[(position()='1' and attribute::uri='cic:/Rocq/LAMBDA/Marks/unmark.con')] and count(child::*) = 2]" mode="pure">
-	<m:apply>
-         <m:csymbol definitionURL="{CONST/@uri}">forgetful</m:csymbol>
-         <xsl:apply-templates select="*[2]" mode="pure"/>
-        </m:apply>
-</xsl:template>
-
-<!-- boolean algebra of redexes -->
-
-<xsl:template match="APPLY[MUTIND[(position()='1' and attribute::uri='cic:/Rocq/LAMBDA/Redexes/sub.ind')] and count(child::*) = 3]" mode="pure">
-	<m:apply>
-         <m:subset definitionURL="{MUTIND/@uri}"/>
-         <xsl:apply-templates select="*[2]" mode="pure"/>
-         <xsl:apply-templates select="*[3]" mode="pure"/>
-        </m:apply>
-</xsl:template>
-
-<xsl:template match="APPLY[MUTIND[(position()='1' and attribute::uri='cic:/Rocq/LAMBDA/Redexes/union.ind')] and count(child::*) = 4]" mode="pure">
-	<m:apply>
-         <m:eq definitionURL="{MUTIND/@uri}"/>
-         <m:apply>
-          <m:union definitionURL="{MUTIND/@uri}"/>
-          <xsl:apply-templates select="*[2]" mode="pure"/>
-          <xsl:apply-templates select="*[3]" mode="pure"/>
-         </m:apply>
-         <xsl:apply-templates select="*[4]" mode="pure"/>
-        </m:apply>
-</xsl:template>
-
-<xsl:template match="APPLY[MUTIND[(position()='1' and attribute::uri='cic:/Rocq/LAMBDA/Redexes/comp.ind')] and count(child::*) = 3]" mode="pure">
-	<m:apply>
-         <m:csymbol definitionURL="{MUTIND/@uri}">isomorphic</m:csymbol>
-         <xsl:apply-templates select="*[2]" mode="pure"/>
-         <xsl:apply-templates select="*[3]" mode="pure"/>
-        </m:apply>
-</xsl:template>
-
-<xsl:template match="APPLY[MUTIND[(position()='1' and attribute::uri='cic:/Rocq/LAMBDA/Residuals/residuals.ind')] and count(child::*) = 4]" mode="pure">
-	<m:apply>
-         <m:eq definitionURL="{MUTIND/@uri}"/>
-         <m:apply>
-          <m:setdiff definitionURL="{MUTIND/@uri}"/>
-          <xsl:apply-templates select="*[2]" mode="pure"/>
-          <xsl:apply-templates select="*[3]" mode="pure"/>
-         </m:apply>
-         <xsl:apply-templates select="*[4]" mode="pure"/>
-        </m:apply>
-</xsl:template>
-
-</xsl:stylesheet>