X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FR%2FRexp.ma;fp=helm%2Fsoftware%2Fmatita%2Flibrary%2FR%2FRexp.ma;h=23b0c5cbb1927e4b278ed316bd3ed6d9d2999ad0;hb=e78cf74f8976cf0ca554f64baa9979d0423ee927;hp=7cea392591ba9156589218480afed0bcc6d6e988;hpb=c6094ab9349aaa41a8c29c5773a3e756ac819e7f;p=helm.git

diff --git a/helm/software/matita/library/R/Rexp.ma b/helm/software/matita/library/R/Rexp.ma
index 7cea39259..23b0c5cbb 100644
--- a/helm/software/matita/library/R/Rexp.ma
+++ b/helm/software/matita/library/R/Rexp.ma
@@ -285,4 +285,4 @@ lemma aaa : ∀x,y:R.R1 < x → lub (expcut x y) (Rexp x y ?).
   |simplify;rewrite > H1 in H;elim (irrefl_Rlt ? H)]]
 qed.*)
 
-interpretation "real numbers exponent" 'exp a b = (Rexp a b _).
+interpretation "real numbers exponent" 'exp a b = (Rexp a b ?).