Mercurial > cpdt > repo

diff src/Predicates.v @ 54:31622083ad5d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Spell-check
author Adam Chlipala <adamc@hcoop.net>
date Sun, 28 Sep 2008 13:13:26 -0400
parents 422865e240b1
children 8d7a97b3bb91
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.
 
   (** [[