This commit was manufactured by cvs2svn to create branch

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

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