From d42e5b087a231f25c06f370a0ae0048ddf76ca7e Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 20 Mar 2001 17:17:28 +0000
Subject: [PATCH] added notation for arithmetics
---
helm/style/basic.xsl | 38 +++-----------------------------------
helm/style/rootcontent.xsl | 5 +++--
2 files changed, 6 insertions(+), 37 deletions(-)
diff --git a/helm/style/basic.xsl b/helm/style/basic.xsl
index 3e385b680..ed6681af2 100644
--- a/helm/style/basic.xsl
+++ b/helm/style/basic.xsl
@@ -27,7 +27,7 @@
<!--******************************************************************-->
<!-- Basic Logic -->
<!-- First draft: April 3 2000 -->
-<!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena -->
+<!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena, Guidi -->
<!--******************************************************************-->
<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
@@ -228,40 +228,9 @@ and (count(child::*) = 2) and APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Logic_T
<!-- no datatypes in MathML content -->
+<!-- ************************** PEANO ********************************* -->
-<!-- *************************** PEANO ********************************* -->
-
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Peano/le.ind'] and (count(child::*) = 3)]" mode="pure">
- <m:apply helm:xref="{@id}">
- <m:leq definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
- <xsl:apply-templates select="*[2]" mode="noannot"/>
- <xsl:apply-templates select="*[3]" mode="noannot"/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Peano/lt.con'] and (count(child::*) = 3)]" mode="pure">
- <m:apply helm:xref="{@id}">
- <m:lt definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
- <xsl:apply-templates select="*[2]" mode="noannot"/>
- <xsl:apply-templates select="*[3]" mode="noannot"/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Peano/ge.con'] and (count(child::*) = 3)]" mode="pure">
- <m:apply helm:xref="{@id}">
- <m:geq definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
- <xsl:apply-templates select="*[2]" mode="noannot"/>
- <xsl:apply-templates select="*[3]" mode="noannot"/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Peano/gt.con'] and (count(child::*) = 3)]" mode="pure">
- <m:apply helm:xref="{@id}">
- <m:gt definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
- <xsl:apply-templates select="*[2]" mode="noannot"/>
- <xsl:apply-templates select="*[3]" mode="noannot"/>
- </m:apply>
-</xsl:template>
+<!-- see arith.xsl --> <!-- FG -->
</xsl:stylesheet>
@@ -269,4 +238,3 @@ and (count(child::*) = 2) and APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Logic_T
-
diff --git a/helm/style/rootcontent.xsl b/helm/style/rootcontent.xsl
index e7197b271..41608e5c4 100644
--- a/helm/style/rootcontent.xsl
+++ b/helm/style/rootcontent.xsl
@@ -27,7 +27,7 @@
<!--***********************************************************************-->
<!-- XSLT version 0.1 of the stylesheet to accomplish the right inclusion -->
<!-- of the content stylesheets: -->
-<!-- First draft: May 26 2000, Claudio Sacerdoti Coen, Irene Schena -->
+<!-- First draft: May 26 2000, C.Sacerdoti Coen, I.Schena, F.Guidi -->
<!--***********************************************************************-->
<!-- Schema of stylesheet precedences (from highest to lowest): -->
@@ -56,8 +56,9 @@
<xsl:variable name="CICAnnotations" select="document(concat($absPath,$CICURI,'.ann'))"/>
<xsl:import href="annotatedcont.xsl"/>
-
+<xsl:include href="contentlib.xsl"/> <!-- FG -->
<xsl:include href="basic.xsl"/>
+<xsl:include href="arith.xsl"/> <!-- FG -->
<xsl:include href="set.xsl"/>
<xsl:include href="reals.xsl"/>
<xsl:include href="proofs.xsl"/>
--
2.39.2