X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fnuprl_stylesheets%2Fnuprl_abstract.xsl;fp=helm%2Fnuprl_stylesheets%2Fnuprl_abstract.xsl;h=0000000000000000000000000000000000000000;hb=c7514aaa249a96c5fdd39b1123fbdb38d92f20b6;hp=fa6d8154d6303851c2f186e2fa611ac46c71dd9e;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;p=helm.git

diff --git a/helm/nuprl_stylesheets/nuprl_abstract.xsl b/helm/nuprl_stylesheets/nuprl_abstract.xsl
deleted file mode 100644
index fa6d8154d..000000000
--- a/helm/nuprl_stylesheets/nuprl_abstract.xsl
+++ /dev/null
@@ -1,170 +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">
-
-
-<xsl:template match="term">
-  <xsl:choose>
-  
-  <xsl:when test="@opid=&quot;le&quot;">
-    <m:apply>
-      <m:leq definitionURL="{@uri}"/>
-        <xsl:apply-templates select="*"/>
-    </m:apply>
-  </xsl:when>
- 
-  <xsl:when test="string(@opid)=&quot;exists&quot;">
-    <m:apply>
-      <m:exists definitionURL="{@uri}"/>
-      <m:bvar>
-        <m:ci>
-	  <xsl:value-of select="binder[1]/@var"/>
-	</m:ci>
-      </m:bvar>
-      <m:condition>
-        <xsl:apply-templates select="*[1]"/>
-      </m:condition>
-      <xsl:apply-templates select="*[3]"/>
-    </m:apply>
-  </xsl:when>
-  
-  <xsl:when test="string(@opid)=&quot;all&quot;">
-    <m:apply>
-      <m:csymbol definitionURL="{@uri}">forall</m:csymbol>
-      <m:bvar>
-        <m:ci>
-          <xsl:value-of select="binder[1]/@var"/>
-        </m:ci>
-        <m:type>
-          <xsl:apply-templates select="*[1]"/>
-        </m:type>
-      </m:bvar>
-      <xsl:apply-templates select="*[3]"/>
-    </m:apply>
-  </xsl:when>
-
-  <xsl:when test="string(@opid)=&quot;and&quot;">
-    <m:apply>
-      <m:and definitionURL="{@uri}"/>
-      <xsl:apply-templates select="*[1]"/>
-      <xsl:apply-templates select="*[2]"/>
-    </m:apply>
-  </xsl:when>
-  
-  <xsl:when test="string(@opid)=&quot;or&quot;">
-    <m:apply>
-      <m:or definitionURL="{@uri}"/>
-      <xsl:apply-templates select="*[1]"/>
-      <xsl:apply-templates select="*[2]"/>
-    </m:apply>
-  </xsl:when>
-  
-  <xsl:when test="string(@opid)=&quot;member&quot;">
-    <m:apply>
-      <m:in definitionURL="{@uri}"/>
-      <xsl:apply-templates select="*[2]"/>
-      <xsl:apply-templates select="*[1]"/>
-    </m:apply>
-  </xsl:when>
-    
-  <xsl:when test="string(@opid)=&quot;implies&quot;">
-    <m:apply>
-      <m:implies definitionURL="{@uri}"/>
-      <xsl:apply-templates select="*[1]"/>
-      <xsl:apply-templates select="*[2]"/>
-    </m:apply>
-  </xsl:when>
-  
-  <xsl:when test="string(@opid)=&quot;not&quot;">
-    <m:apply>
-      <m:not definitionURL="{@uri}"/>
-      <xsl:apply-templates select="*[1]"/>
-    </m:apply>
-  </xsl:when>
-  
-  <xsl:when test="string(@opid)=&quot;nat&quot;">
-    <m:naturalnumbers definitionURL="{@uri}"/>
-  </xsl:when>
-  
-  <xsl:when test="string(@opid)=&quot;so_lambda&quot;">
-    <m:apply>
-      <m:csymbol definitionURL="{@uri}">so_lambda</m:csymbol>
-      <xsl:choose>
-      <xsl:when test="*[1]=so_variable">
-        <m:apply>
-        <m:ci>so_variable</m:ci>
-        <m:ci>
-          <xsl:value-of select="so_variable/@var"/>
-	</m:ci>
-        </m:apply>
-        <!--<xsl:apply-templates select="*[2]"/>
-        <xsl:apply-templates select="*[3]"/>-->
-        <xsl:apply-templates/>
-      </xsl:when>
-      <xsl:otherwise>
-        <xsl:apply-templates select="*[1]"/>
-        <xsl:apply-templates select="*[2]"/>
-      </xsl:otherwise>
-      </xsl:choose>
-    </m:apply>
-  </xsl:when>
-  
-  <xsl:when test="string(@opid)=&quot;so_apply&quot;">
-    <m:apply>
-      <m:csymbol definitionURL="{@uri}">so_apply</m:csymbol>
-      <xsl:apply-templates select="*[1]"/>
-      <xsl:apply-templates select="*[2]"/>
-    </m:apply>
-  </xsl:when>	
-  
-  <xsl:when test="string(@opid)=&quot;gcd_p&quot;">
-    <m:apply>
-      <m:ci definitionURL="{@uri}">gcd_p</m:ci>
-      <xsl:apply-templates/>
-    </m:apply>
-  </xsl:when>
-  
-  <xsl:when test="string(@opid)=&quot;decidable&quot;">
-    <m:apply>
-      <m:ci definitionURL="{@uri}">decidable</m:ci>
-      <xsl:apply-templates/>
-    </m:apply>
-  </xsl:when>
-  
-  <xsl:when test="string(@opid)=&quot;int_seg&quot;">
-    <m:interval definitionURL="{@uri}">
-      <xsl:apply-templates select="*[1]"/>
-      <xsl:apply-templates select="*[2]"/>
-    </m:interval>
-  </xsl:when>
-  <xsl:when test="string(@opid)=&quot;ge&quot;">
-    <m:apply>
-      <m:geq definitionURL="{@uri}"/>
-      <xsl:apply-templates select="*[1]"/>
-      <xsl:apply-templates select="*[2]"/>
-    </m:apply>
-  </xsl:when>
-  
-  <xsl:when test="string(@opid)=&quot;false&quot;">
-    <m:false definitionURL="{@uri}"/>
-  </xsl:when>
-  
-  <xsl:when test="string(@opid)=&quot;true&quot;">
-    <m:true definitionURL="{@uri}"/>
-  </xsl:when>
-  
-    <!-- ALTRE ASTRAZIONI -->
-  <xsl:otherwise>
-    <m:apply>
-     <m:csymbol>app</m:csymbol>
-     <m:ci definitionURL="{@uri}">
-       <xsl:value-of select="@opid"/>
-     </m:ci>
-     <xsl:apply-templates/>
-    </m:apply>
-  </xsl:otherwise>
-  
-  </xsl:choose>
-  
-</xsl:template>
-
-</xsl:stylesheet>