diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-25 07:56:54 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-25 07:56:54 +0000 |
| commit | 7da3cb6694b0584f8e01e8c75ca93ff63d8984f0 (patch) | |
| tree | 9f4dbdff9443a730e763eca29f4fef38e0a146a0 /theories/Reals/Rseries.v | |
| parent | b002b817ce305be3ba753dc1634a01b008b243bd (diff) | |
coqweb
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1711 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rseries.v')
| -rw-r--r-- | theories/Reals/Rseries.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index 2e94528d5..a388e2ae3 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -12,7 +12,7 @@ Require Export Rderiv. Require Classical. Require Compare. -(* classical is needed for Un_cv_crit *) +(* classical is needed for [Un_cv_crit] *) (*********************************************************) (* Definition of sequence and properties *) (* *) @@ -84,7 +84,7 @@ Unfold ge in H0;Generalize (H0 (S n0) H1 (lt_le_S n0 n1 y));Intro; Save. -(* classical is needed: not_all_not_ex *) +(* classical is needed: [not_all_not_ex] *) (*********) Lemma Un_cv_crit:Un_growing->(bound EUn)->(ExT [l:R] (Un_cv l)). Unfold Un_growing Un_cv;Intros; |