First version of Di Lena's stylesheet generator (for the HELM DTD).

[helm.git] / helm / meta_style / reals.xml

diff --git a/helm/meta_style/reals.xml b/helm/meta_style/reals.xml
new file mode 100644 (file)
index 0000000..b4cdf2d
--- /dev/null
+++ b/helm/meta_style/reals.xml
@@ -0,0 +1,163 @@
+<!DOCTYPE OpList SYSTEM "operator.dtd">
+
+<OpList xmlns:m="http://www.w3.org/1998/Math/MathML">
+
+<!-- Unary Operations and power -->
+
+<Operator
+ name  = "0"
+ uri   = "cic:/Coq/Reals/Rdefinitions/R0.con">
+       <mop tag="cn">0</mop>
+</Operator>
+
+<Operator
+ name  = "1"
+ uri   = "cic:/Coq/Reals/Rdefinitions/R1.con">
+       <mop tag="cn">1</mop>
+</Operator>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Coq/Reals/Rdefinitions/Ropp.con"
+ arity = "1"
+ m-tag = "minus"/>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Coq/Reals/Rbasic_fun/Rabsolu.con"
+ arity = "1"
+ m-tag = "abs"/>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Coq/Reals/Rfunctions/fact.con"
+ arity = "1"
+ m-tag = "factorial"/>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Coq/Reals/Rbase/Rsqr.con"
+ arity = "1">
+       <mapp>
+               <mop tag="power"/>
+               <param id="1"/>
+               <m:cn>2</m:cn>
+       </mapp>
+</Operator>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Coq/Reals/Rdefinitions/Rinv.con"
+ arity = "1">
+       <mapp>
+               <mop tag="power"/>
+               <param id="1"/>
+               <mapp>
+                       <mop tag="minus"/>
+                       <m:cn>1</m:cn>
+               </mapp>
+       </mapp>
+</Operator>
+
+<!-- Binary Operations and Relations -->
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Coq/Reals/Rdefinitions/Rle.con"
+ arity = "2"
+ m-tag = "leq"/>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Coq/Reals/Rdefinitions/Rlt.con"
+ arity = "2"
+ m-tag = "lt"/>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Coq/Reals/Rdefinitions/Rge.con"
+ arity = "2"
+ m-tag = "geq"/>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Coq/Reals/Rdefinitions/Rgt.con"
+ arity = "2"
+ m-tag = "gt"/>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Coq/Reals/Rdefinitions/Rplus.con"
+ arity = "2"
+ m-tag = "plus"/>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Coq/Reals/Rdefinitions/Rminus.con"
+ arity = "2"
+ m-tag = "minus"/>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Coq/Reals/Rdefinitions/Rmult.con"
+ arity = "2"
+ m-tag = "times"/>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Coq/Reals/Rdefinitions/Rdiv.con"
+ arity = "2"
+ m-tag = "divide"/>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Coq/Reals/Rbasic_fun/Rmin.con"
+ arity = "2"
+ m-tag = "min"/>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Coq/Reals/Rbasic_fun/Rmax.con"
+ arity = "2"
+ m-tag = "max"/>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Coq/Reals/Rfunctions/pow.con"
+ arity = "2"
+ m-tag = "power"/>
+
+<Operator
+ name  = "LIMIT"
+ uri   = "cic:/Coq/Reals/Rlimit/limit1_in.con"
+ arity = "4">
+       <m:apply>
+               <m:eq/>
+               <mapp>
+                       <mop tag="limit"/>
+                       <mbvar name="x"/>
+                       <m:lowlimit>
+                               <param id="4"/>
+                       </m:lowlimit>
+                       <param id="1" bvar="x"/>
+               </mapp>
+               <param id="3"/>
+       </m:apply>
+</Operator>
+
+<Operator
+ name  = "DIFFERENTIATION"
+ uri   = "cic:/Coq/Reals/Rderiv/D_in.con"
+ arity = "3">
+       <m:apply>
+               <m:eq/>
+               <mapp>
+                       <mop tag="diff"/>
+                       <mbvar name="x"/>
+                       <param id="1" bvar="x"/>
+               </mapp>
+               <param id="3"/>
+       </m:apply>
+</Operator>
+
+</OpList>