This commit was manufactured by cvs2svn to create branch

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

diff --git a/helm/meta_style/arith.xml b/helm/meta_style/arith.xml
deleted file mode 100644 (file)
index 17fc523..0000000
--- a/helm/meta_style/arith.xml
+++ /dev/null
@@ -1,69 +0,0 @@
-<!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>