## 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 *)