Mercurial > cpdt > repo

diff src/Predicates.v @ 67:55199444e5e7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finish Coinductive chapter
author Adam Chlipala <adamc@hcoop.net>
date Wed, 01 Oct 2008 09:56:32 -0400
parents b581446229fd
children 8caa3b3f8fc0
line wrap: on
line diff
--- a/src/Predicates.v	Wed Oct 01 09:33:44 2008 -0400
+++ b/src/Predicates.v	Wed Oct 01 09:56:32 2008 -0400
@@ -358,7 +358,7 @@
 
 Theorem exist1 : exists x : nat, x + 1 = 2.
 (* begin thide *)
-  (** remove printing exists*)
+  (** remove printing exists *)
   (** We can start this proof with a tactic [exists], which should not be confused with the formula constructor shorthand of the same name.  (In the PDF version of this document, the reverse 'E' appears instead of the text "exists" in formulas.) *)
   exists 1.