Mercurial > cpdt > repo
diff src/Subset.v @ 76:82a2189fa283
Spell check
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Fri, 03 Oct 2008 15:11:44 -0400 |
parents | ec2c1830a7a1 |
children | d07c77659c20 |
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. (** [[