X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fmeta_style%2Freals.xml;fp=helm%2Fmeta_style%2Freals.xml;h=0000000000000000000000000000000000000000;hp=b4cdf2d8a7ff912f8b26ac00d734c1f5a8c3dbee;hb=3ef089a4c58fbe429dd539af6215991ecbe11ee2;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff

diff --git a/helm/meta_style/reals.xml b/helm/meta_style/reals.xml
deleted file mode 100644
index b4cdf2d8a..000000000
--- 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>