]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/nuprl_stylesheets/nuprl_abstract.xsl
This commit was manufactured by cvs2svn to create branch
[helm.git] / helm / nuprl_stylesheets / nuprl_abstract.xsl
diff --git a/helm/nuprl_stylesheets/nuprl_abstract.xsl b/helm/nuprl_stylesheets/nuprl_abstract.xsl
deleted file mode 100644 (file)
index fa6d815..0000000
+++ /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>