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.
 (** [[