]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/meta_style/algebra.xml
First version of Di Lena's stylesheet generator (for the HELM DTD).
[helm.git] / helm / meta_style / algebra.xml
diff --git a/helm/meta_style/algebra.xml b/helm/meta_style/algebra.xml
new file mode 100644 (file)
index 0000000..119effa
--- /dev/null
@@ -0,0 +1,204 @@
+<!DOCTYPE OpList SYSTEM "operator.dtd">
+
+<OpList xmlns:m="http://www.w3.org/1998/Math/MathML">
+
+<!-- Unary Operations -->
+
+<Operator
+ name  = "0"
+ uri   = "cic:/Algebra/CSemiGroups/csg_unit.con"
+ arity = "1">
+       <mop tag="ci" helm:xref="$APP-ID">0</mop>
+</Operator>
+
+<Operator
+ name  = "1"
+ uri   = "cic:/Algebra/CRings/cr_one.con"
+ arity = "1">
+       <mop tag="ci" helm:xref="$APP-ID">1</mop>
+</Operator>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Algebra/CGroups/cg_inv.con"
+ hide  = "1"
+ arity = "1"
+ m-tag = "minus"/>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Algebra/CMetricFields/CMetric_Fields/cmf_abs.con"
+ hide  = "1"
+ arity = "2"
+ m-tag = "abs"/>
+
+<!-- Binary Operations and Relations -->
+
+<Operator
+ name  = "SETOID EQUALITY"
+ uri   = "cic:/Algebra/CSetoids/cs_eq.con"
+ hide  = "1"
+ arity = "2"
+ m-tag = "eq"/>
+
+<Operator
+ name  = "APART"
+ uri   = "cic:/Algebra/CSetoids/cs_ap.con"
+ hide  = "1"
+ arity = "2"
+ m-tag = "neq"/>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Algebra/COrdFields/leEq.con"
+ hide  = "1"
+ arity = "2"
+ m-tag = "leq"/>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Algebra/COrdFields/cof_less.con"
+ hide  = "1"
+ arity = "2"
+ m-tag = "lt"/>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Algebra/CRings/cr_plus.con | cic:/Algebra/CSemiGroups/csg_op.con"
+ hide  = "1"
+ arity = "2"
+ m-tag = "plus"/>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Algebra/CRings/cr_minus.con | cic:/Algebra/CGroups/cg_minus.con"
+ hide  = "1"
+ arity = "2"
+ m-tag = "minus"/>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Algebra/CRings/cr_mult.con"
+ hide  = "1"
+ arity = "2"
+ m-tag = "times"/>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Algebra/CFields/cf_div.con"
+ hide  = "1"
+ arity = "2"
+ m-tag = "divide"/>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Algebra/CRings/Ring_constructions/nzpro.con"
+ cook  = "true"
+ arity = "2">
+       <param id="1"/>
+</Operator>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Algebra/CRings/exponentiation/nexp.con"
+ cook  = "true"
+ arity = "2"
+ m-tag = "power"/>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Algebra/CRings/exponentiation/nexp_op.con | cic:/Algebra/Expon/Zexp_def/zexp.con"
+ cook  = "true"
+ arity = "2">
+       <mapp>
+               <mop tag="power"/>
+               <param id="2"/>
+               <param id="1"/>
+       </mapp>
+</Operator>
+
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Algebra/COrdFields/absSmall.con"
+ hide  = "1"
+ arity = "2">
+       <mapp>
+               <mop tag="lt"/>
+               <mapp>
+                       <mop tag="abs"/>
+                       <param id="2"/>
+               </mapp>
+               <param id="1"/>
+       </mapp>
+</Operator>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Algebra/CPolynomials/CPoly_CRing_ctd/cpoly_apply_fun.con"
+ cook  = "true"
+ arity = "2"> 
+       <mapp>
+               <m:csymbol>app</m:csymbol>
+               <param id="1"/>
+               <param id="2"/>
+       </mapp>
+</Operator>
+
+<Operator
+ name  = "********"
+ uri   = "cic:/Algebra/COrdFields/OrdField_Cauchy/seqLimit.con"
+ cook  = "true"
+ arity = "2">
+       <mapp>
+               <mop tag="eq" helm:xref="$APP-ID"/>
+               <mapp helm:xref="$OP-ID">
+                       <mop tag="limit"/>
+                       <mbvar name="x"/>
+                       <m:lowlimit>
+                               <m:infinity/>
+                       </m:lowlimit>
+                       <param id="1" bvar="x"/>
+               </mapp>
+               <param id="2"/>
+       </mapp>
+</Operator>
+
+<Operator
+ name  = "********"
+ uri   = "cic:/Algebra/CSums/Sums/sum0.con"
+ cook  = "true"
+ arity = "2">
+       <m:apply helm:xref="$OP-ID">
+               <mop tag="sum"/>
+               <mbvar name="x"/>
+               <m:condition>
+                       <m:apply>
+                               <m:lt/>
+                               <mvar name="x"/>
+                               <param id="1"/>
+                       </m:apply>
+               </m:condition>
+               <param id="2" bvar="x"/>
+       </m:apply>
+</Operator>
+
+<Operator
+ name  = "SUM"
+ uri   = "cic:/Algebra/CSums/Sums/sum.con"
+ cook  = "true"
+ arity = "3">
+       <m:apply helm:xref="$OP-ID">
+               <mop tag="sum"/>
+               <mbvar name="x"/>
+               <m:lowlimit>
+                       <param id="1"/>
+               </m:lowlimit>
+               <m:uplimit>
+                       <param id="2"/>
+               </m:uplimit>
+               <param id="3" bvar="x"/>
+       </m:apply>
+</Operator>
+
+</OpList>