Mercurial > cpdt > repo
diff src/Predicates.v @ 470:0df6dde807ab
Batch of changes based on proofreader feedback
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Tue, 02 Oct 2012 11:34:40 -0400 |
| parents | b36876d4611e |
| children | 51a8472aca68 |
line wrap: on
line diff
--- a/src/Predicates.v Wed Sep 26 16:35:35 2012 -0400 +++ b/src/Predicates.v Tue Oct 02 11:34:40 2012 -0400 @@ -380,7 +380,7 @@ Theorem exist1 : exists x : nat, x + 1 = 2. (* begin thide *) (** remove printing exists *) - (** We can start this proof with a tactic %\index{tactics!exists}%[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.) *) + (** We can start this proof with a tactic %\index{tactics!exists}%[exists], which should not be confused with the formula constructor shorthand of the same name. %In the version of this document that you are reading, the reverse ``E'' appears instead of the text ``exists'' in formulas.% *) exists 1.