Mercurial > cpdt > repo
changeset 54:31622083ad5d
Spell-check
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 28 Sep 2008 13:13:26 -0400 |
parents | 422865e240b1 |
children | 8d7a97b3bb91 |
files | src/Predicates.v |
diffstat | 1 files changed, 1 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Predicates.v Sun Sep 28 12:44:50 2008 -0400 +++ b/src/Predicates.v Sun Sep 28 13:13:26 2008 -0400 @@ -670,7 +670,7 @@ Lemma even_contra' : forall n', even n' -> forall n, n' = S (n + n) -> False. induction 1; crush. - (** At this point, it is useful to consider all cases of [n] and [n0] being zero or nonzero. Only one of these cases has any trickyness to it. *) + (** At this point, it is useful to consider all cases of [n] and [n0] being zero or nonzero. Only one of these cases has any trickiness to it. *) destruct n; destruct n0; crush. (** [[