Mercurial > cpdt > repo

diff src/Predicates.v @ 210:b149a07b9b5b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Most old Sestoft suggestions processed
author Adam Chlipala <adamc@hcoop.net>
date Mon, 09 Nov 2009 13:18:46 -0500
parents 90af611e2993
children c4b1c0de7af9
line wrap: on
line diff
--- a/src/Predicates.v	Mon Nov 09 11:48:27 2009 -0500
+++ b/src/Predicates.v	Mon Nov 09 13:18:46 2009 -0500
@@ -134,7 +134,7 @@
  
   ]]
   
-  The interested reader can check that [and] has a Curry-Howard doppleganger called [prod], the type of pairs.  However, it is generally most convenient to reason about conjunction using tactics.  An explicit proof of commutativity of [and] illustrates the usual suspects for such tasks.  [/\] is an infix shorthand for [and]. *)
+  The interested reader can check that [and] has a Curry-Howard doppelganger called [prod], the type of pairs.  However, it is generally most convenient to reason about conjunction using tactics.  An explicit proof of commutativity of [and] illustrates the usual suspects for such tasks.  [/\] is an infix shorthand for [and]. *)
 
   Theorem and_comm : P /\ Q -> Q /\ P.