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

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

diff --git a/helm/meta_style/arith.xml b/helm/meta_style/arith.xml
new file mode 100644 (file)
index 0000000..17fc523
--- /dev/null
+++ b/helm/meta_style/arith.xml
@@ -0,0 +1,69 @@
+<!DOCTYPE OpList SYSTEM "operator.dtd">
+
+<!-- ************************** ARITHMETICS ****************************** -->
+
+<OpList xmlns:m="http://www.w3.org/1998/Math/MathML">
+
+<import href="positive.xsl"/>
+
+<Operator
+ name  = "LESS EQUAL"
+ uri   = "cic:/Coq/Init/Peano/le.ind | cic:/Coq/ZArith/zarith_aux/Zle.con"
+ arity = "2"
+ m-tag = "leq"/>
+
+<Operator
+ name  = "LESS THAN"
+ uri   = "cic:/Coq/Init/Peano/lt.con | cic:/Coq/ZArith/zarith_aux/Zlt.con"
+ arity = "2"
+ m-tag = "lt"/>
+
+<Operator
+ name  = "GREATER EQUAL"
+ uri   = "cic:/Coq/Init/Peano/ge.con | cic:/Coq/ZArith/zarith_aux/Zge.con"
+ arity = "2"
+ m-tag = "geq"/>
+
+<Operator
+ name  = "GREATER THAN"
+ uri   = "cic:/Coq/Init/Peano/gt.con | cic:/Coq/ZArith/zarith_aux/Zgt.con"
+ arity = "2"
+ m-tag = "gt"/>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Coq/Init/Peano/plus.con | cic:/Coq/ZArith/fast_integer/fast_integers/Zplus.con"
+ arity = "2"
+ m-tag = "plus"/>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Coq/Arith/Minus/minus.con | cic:/Coq/ZArith/zarith_aux/Zminus.con"
+ arity = "2"
+ m-tag = "minus"/>
+ 
+<Operator
+ name  = "*****"
+ uri   = "cic:/Coq/Init/Peano/mult.con | cic:/Coq/ZArith/fast_integer/fast_integers/Zmult.con"
+ arity = "2"
+ m-tag = "times"/>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Coq/Arith/Min/min.con | cic:/Coq/ZArith/zarith_aux/Zmin.con"
+ arity = "2"
+ m-tag = "min"/>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Coq/ZArith/fast_integer/fast_integers/Zopp.con"
+ arity = "1"
+ m-tag = "minus"/>
+
+<Operator
+ name  = "*****"
+ uri   = "cic:/Coq/ZArith/zarith_aux/absolu.con"
+ arity = "1"
+ m-tag = "abs"/>
+                                               
+</OpList>