diff src/Predicates.v @ 448:2740b8a23cce

Proofreading pass through Chapter 3
author Adam Chlipala <adam@chlipala.net>
date Fri, 17 Aug 2012 14:19:59 -0400
parents 89c67796754e
children 79190c225f1a
line wrap: on
line diff
--- a/src/Predicates.v	Fri Aug 17 12:22:26 2012 -0400
+++ b/src/Predicates.v	Fri Aug 17 14:19:59 2012 -0400
@@ -849,7 +849,7 @@
 (* begin hide *)
 (* In-class exercises *)
 
-(* EX: Define a type [prop] of simple boolean formulas made up only of truth, falsehood, binary conjunction, and binary disjunction.  Define an inductive predicate [holds] that captures when [prop]s are valid, and define a predicate [falseFree] that captures when a [prop] does not contain the "false" formula.  Prove that every false-free [prop] is valid. *)
+(* EX: Define a type [prop] of simple Boolean formulas made up only of truth, falsehood, binary conjunction, and binary disjunction.  Define an inductive predicate [holds] that captures when [prop]s are valid, and define a predicate [falseFree] that captures when a [prop] does not contain the "false" formula.  Prove that every false-free [prop] is valid. *)
 
 (* begin thide *)
 Inductive prop : Set :=