Mercurial > cpdt > repo
changeset 76:82a2189fa283
Spell check
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Fri, 03 Oct 2008 15:11:44 -0400 (2008-10-03) |
parents | ec2c1830a7a1 |
children | d07c77659c20 |
files | src/Subset.v |
diffstat | 1 files changed, 1 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Subset.v Fri Oct 03 15:10:30 2008 -0400 +++ b/src/Subset.v Fri Oct 03 15:11:44 2008 -0400 @@ -233,7 +233,7 @@ end); crush. Defined. -(** We end the "proof" with [Defined] instead of [Qed], so that the definition we constructed remains visible. This contrasts to the case of ending a proof with [Qed], where the details of the proof are hidden afterward. Let us see what our prooof script constructed. *) +(** We end the "proof" with [Defined] instead of [Qed], so that the definition we constructed remains visible. This contrasts to the case of ending a proof with [Qed], where the details of the proof are hidden afterward. Let us see what our proof script constructed. *) Print pred_strong4. (** [[