From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 3 Nov 2000 12:13:27 +0000 (+0000)
Subject: Set notation now working again
X-Git-Tag: nogzip~217
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e4ae880d435c1b46be0e900a675d2e6e4aaac837;p=helm.git

Set notation now working again
---

diff --git a/helm/style/rootcontent.xsl b/helm/style/rootcontent.xsl
index 9e85f0344..7776afbbf 100644
--- a/helm/style/rootcontent.xsl
+++ b/helm/style/rootcontent.xsl
@@ -19,7 +19,7 @@
 <xsl:import href="annotatedcont.xsl"/>
 <xsl:key name="id" use="@id" match="LAMBDA|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|Definition|Axiom|CurrentProof|InductiveDefinition|Variable"/>
 <xsl:include href="basic.xsl"/>
-<!-- <xsl:include href="set.xsl"/> -->
+<xsl:include href="set.xsl"/>
 <xsl:include href="reals.xsl"/>
 <xsl:include href="proofs.xsl"/>
 
diff --git a/helm/style/set.xsl b/helm/style/set.xsl
index 303c872ef..b61b44e88 100644
--- a/helm/style/set.xsl
+++ b/helm/style/set.xsl
@@ -46,7 +46,7 @@
 
 <!-- IN -->
 
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/In.con']]" mode="noannot">
+<xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/In.con']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
@@ -72,7 +72,7 @@
 <!-- NOT-IN -->
 <!-- NOT ha no parameters -->
 <xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/INIT/Logic/not.con']
-and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/In.con']]]" mode="noannot">
+and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/In.con']]]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
@@ -96,7 +96,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
 
 <!-- EMPTY SET -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Empty_set.ind']]" mode="noannot">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Empty_set.ind']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
@@ -124,7 +124,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
 
 <!-- SINGLETON -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Singleton.ind']]" mode="noannot">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Singleton.ind']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
@@ -154,7 +154,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
 
 <!-- COUPLE -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Couple.ind']]" mode="noannot">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Couple.ind']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
@@ -186,7 +186,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
 
 <!-- TRIPLE -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Triple.ind'] and (count(child::*) = 5)]" mode="noannot">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Triple.ind'] and (count(child::*) = 5)]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
@@ -220,7 +220,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
 
 <!-- INTERSECTION -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Intersection.ind']]" mode="noannot">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Intersection.ind']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
@@ -255,7 +255,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
 
 <!-- UNION -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Union.ind']]" mode="noannot">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Union.ind']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
@@ -289,7 +289,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
 
 <!-- INCLUDED -->
 
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Included.con']]" mode="noannot">
+<xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Included.con']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
@@ -312,7 +312,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
 
 <!-- STRICTLY INCLUDED -->
 
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Strict_Included.con']]" mode="noannot">
+<xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Strict_Included.con']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
@@ -335,7 +335,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
 
 <!-- SET-DIFF -->
 
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Setminus.con']]" mode="noannot">
+<xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Setminus.con']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
@@ -369,7 +369,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
 
 <!-- ADD-ELEM -->
 
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Add.con']]" mode="noannot">
+<xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Add.con']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
@@ -407,7 +407,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
 
 <!-- SUBTRACT-ELEM -->
 
-<xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Subtract.con']]" mode="noannot">
+<xsl:template match="APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensembles/Ensembles/Subtract.con']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
@@ -445,7 +445,7 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
 
 <!-- CARD -->
 
-<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Finite_sets/Ensembles_finis/cardinal.ind']]" mode="noannot">
+<xsl:template match="APPLY[MUTIND[attribute::uri='cic:/coq/SETS/Finite_sets/Ensembles_finis/cardinal.ind']]" mode="pure">
     <xsl:variable name="no_params">
      <xsl:call-template name="get_no_params">
       <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
@@ -470,18 +470,3 @@ and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/coq/SETS/Ensemble
 </xsl:template>
 
 </xsl:stylesheet>
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-