1 <!DOCTYPE OpList SYSTEM "operator.dtd">
3 <OpList xmlns:m="http://www.w3.org/1998/Math/MathML">
5 <!-- Unary Operations and power -->
9 uri = "cic:/Coq/Reals/Rdefinitions/R0.con">
15 uri = "cic:/Coq/Reals/Rdefinitions/R1.con">
21 uri = "cic:/Coq/Reals/Rdefinitions/Ropp.con"
27 uri = "cic:/Coq/Reals/Rbasic_fun/Rabsolu.con"
33 uri = "cic:/Coq/Reals/Rfunctions/fact.con"
39 uri = "cic:/Coq/Reals/Rbase/Rsqr.con"
50 uri = "cic:/Coq/Reals/Rdefinitions/Rinv.con"
62 <!-- Binary Operations and Relations -->
66 uri = "cic:/Coq/Reals/Rdefinitions/Rle.con"
72 uri = "cic:/Coq/Reals/Rdefinitions/Rlt.con"
78 uri = "cic:/Coq/Reals/Rdefinitions/Rge.con"
84 uri = "cic:/Coq/Reals/Rdefinitions/Rgt.con"
90 uri = "cic:/Coq/Reals/Rdefinitions/Rplus.con"
96 uri = "cic:/Coq/Reals/Rdefinitions/Rminus.con"
102 uri = "cic:/Coq/Reals/Rdefinitions/Rmult.con"
108 uri = "cic:/Coq/Reals/Rdefinitions/Rdiv.con"
114 uri = "cic:/Coq/Reals/Rbasic_fun/Rmin.con"
120 uri = "cic:/Coq/Reals/Rbasic_fun/Rmax.con"
126 uri = "cic:/Coq/Reals/Rfunctions/pow.con"
132 uri = "cic:/Coq/Reals/Rlimit/limit1_in.con"
142 <param id="1" bvar="x"/>
149 name = "DIFFERENTIATION"
150 uri = "cic:/Coq/Reals/Rderiv/D_in.con"
157 <param id="1" bvar="x"/>