Mercurial > cpdt > repo

diff src/Predicates.v @ 488:31258618ef73

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Incorporate feedback from Nathan Collins
author Adam Chlipala <adam@chlipala.net>
date Tue, 08 Jan 2013 14:38:56 -0500
parents 1fd4109f7b31
children 07f2fb4d9b36
line wrap: on
line diff
--- a/src/Predicates.v	Mon Jan 07 15:23:16 2013 -0500
+++ b/src/Predicates.v	Tue Jan 08 14:38:56 2013 -0500
@@ -129,7 +129,7 @@
       : Prop -> Prop
      ]]
 
-     We see that [not] is just shorthand for implication of [False].  We can use that fact explicitly in proofs.  The syntax [~ P] expands to [not P]. *)
+     We see that [not] is just shorthand for implication of [False].  We can use that fact explicitly in proofs.  The syntax [~ P] %(written with a tilde in ASCII)% expands to [not P]. *)
 
   Theorem arith_neq' : ~ (2 + 2 = 5).
 (* begin thide *)