X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Procedural%2Freals%2FRealFuncts.mma;h=fa95a4af128487729f4965e0668600c74e0d14fa;hb=a89360d64f1fcbba917ad743b97a2d973ecf6db2;hp=8ba6e4bb606c9fbb3cd07ba5be11fbfddac591e2;hpb=32e77480c65cbf23ae7dea38a519c83dfeaf3830;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Procedural/reals/RealFuncts.mma b/helm/software/matita/contribs/CoRN-Procedural/reals/RealFuncts.mma
index 8ba6e4bb6..fa95a4af1 100644
--- a/helm/software/matita/contribs/CoRN-Procedural/reals/RealFuncts.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/reals/RealFuncts.mma
@@ -58,15 +58,15 @@ Intervals like $[a,b]$#[a,b]# are defined for arbitrary reals [a,b] (being
 $\emptyset$#∅# for [a [>] b]).
 *)
 
-inline procedural "cic:/CoRN/reals/RealFuncts/Intclr.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/Intclr.con" as definition.
 
-inline procedural "cic:/CoRN/reals/RealFuncts/Intolr.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/Intolr.con" as definition.
 
-inline procedural "cic:/CoRN/reals/RealFuncts/Intol.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/Intol.con" as definition.
 
-inline procedural "cic:/CoRN/reals/RealFuncts/Intcl.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/Intcl.con" as definition.
 
-inline procedural "cic:/CoRN/reals/RealFuncts/Intcr.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/Intcr.con" as definition.
 
 (*#* The limit of [f(x)] as [x] goes to [p = l], for both unary and binary
 functions:
@@ -78,11 +78,11 @@ forall e [>] Zero, exists d [>] Zero, forall (x : IR)
 ]]
 *)
 
-inline procedural "cic:/CoRN/reals/RealFuncts/funLim.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/funLim.con" as definition.
 
 (*#* The definition of limit of [f] in [p] using Cauchy sequences. *)
 
-inline procedural "cic:/CoRN/reals/RealFuncts/funLim_Cauchy.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/funLim_Cauchy.con" as definition.
 
 (*#* The first definition implies the second one. *)
 
@@ -111,40 +111,40 @@ forall e [>] Zero, exists d [>] Zero, forall (x : IR)
 ]]
 *)
 
-inline procedural "cic:/CoRN/reals/RealFuncts/funLim2.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/funLim2.con" as definition.
 
 (*#* The function [f] is continuous at [p] if the limit of [f(x)] as
 [x] goes to [p] is [f(p)].  This is the [eps [/] delta] definition.
 We also give the definition with limits of Cauchy sequences.
 *)
 
-inline procedural "cic:/CoRN/reals/RealFuncts/continAt.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/continAt.con" as definition.
 
-inline procedural "cic:/CoRN/reals/RealFuncts/continAtCauchy.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/continAtCauchy.con" as definition.
 
-inline procedural "cic:/CoRN/reals/RealFuncts/continAt2.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/continAt2.con" as definition.
 
 (*
 Ax_iom continAt_prop1 :(p:IR)(continAt p)->(continAtCauchy p).
 *)
 
-inline procedural "cic:/CoRN/reals/RealFuncts/contin.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/contin.con" as definition.
 
-inline procedural "cic:/CoRN/reals/RealFuncts/continCauchy.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/continCauchy.con" as definition.
 
-inline procedural "cic:/CoRN/reals/RealFuncts/contin2.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/contin2.con" as definition.
 
 (*#*
 Continuous on a closed, resp.%\% open, resp.%\% left open, resp.%\% left closed
 interval *)
 
-inline procedural "cic:/CoRN/reals/RealFuncts/continOnc.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/continOnc.con" as definition.
 
-inline procedural "cic:/CoRN/reals/RealFuncts/continOno.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/continOno.con" as definition.
 
-inline procedural "cic:/CoRN/reals/RealFuncts/continOnol.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/continOnol.con" as definition.
 
-inline procedural "cic:/CoRN/reals/RealFuncts/continOncl.con".
+inline procedural "cic:/CoRN/reals/RealFuncts/continOncl.con" as definition.
 
 (*
 Section Sequence_and_function_limits.