diff options
Diffstat (limited to 'theories/Reals/Rpower.v')
| -rw-r--r-- | theories/Reals/Rpower.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index 30dfa62742..d850d7f895 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -195,13 +195,13 @@ apply Rinv_neq_0_compat; red in |- *; intro; rewrite H3 in H; Qed. (* Definition of log R+* -> R *) -Boxed Definition Rln (y:posreal) : R := +Definition Rln (y:posreal) : R := match ln_exists (pos y) (cond_pos y) with | existT a b => a end. (* Extension on R *) -Boxed Definition ln (x:R) : R := +Definition ln (x:R) : R := match Rlt_dec 0 x with | left a => Rln (mkposreal x a) | right a => 0 @@ -377,7 +377,7 @@ Qed. (* Definition of Rpower *) (******************************************************************) -Boxed Definition Rpower (x y:R) := exp (y * ln x). +Definition Rpower (x y:R) := exp (y * ln x). Infix Local "^R" := Rpower (at level 30, right associativity) : R_scope. |