diff options
| author | herbelin | 2003-11-29 16:09:14 +0000 |
|---|---|---|
| committer | herbelin | 2003-11-29 16:09:14 +0000 |
| commit | 95ad10e5eb2efc9b63382e0e6a2f9ada8da2ea2d (patch) | |
| tree | 4480983491e88fa3e52703de7853c642387fc676 | |
| parent | 4b999c918bddfd24b4e67e8eb699baa3abf9e2ed (diff) | |
Notation locale pour Rpower
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5025 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/Reals/Rpower.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index 10301bf6e8..c4cb1a8eb4 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -326,6 +326,8 @@ Qed. Definition Rpower := [x : R] [y : R] ``(exp (y*(ln x)))``. +Infix Local "^R" Rpower (at level 2, left associativity) : R_scope. + (******************************************************************) (* Properties of Rpower *) (******************************************************************) |