Mercurial > cpdt > repo
diff src/Large.v @ 350:ad315efc3b6b
Stub out new chapter
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 26 Oct 2011 11:19:52 -0400 |
parents | d5787b70cf48 |
children | b809d3a8a5b1 |
line wrap: on
line diff
--- a/src/Large.v Tue Oct 25 10:56:00 2011 -0400 +++ b/src/Large.v Wed Oct 26 11:19:52 2011 -0400 @@ -284,7 +284,7 @@ Before we are ready to update our proofs, we need to write them in the first place. While fully-automated scripts are most robust to changes of specification, it is hard to write every new proof directly in that form. Instead, it is useful to begin a theorem with exploratory proving and then gradually refine it into a suitable automated form. - Consider this theorem from Chapter 7, which we begin by proving in a mostly manual way, invoking [crush] after each steop to discharge any low-hanging fruit. Our manual effort involves choosing which expressions to case-analyze on. *) + Consider this theorem from Chapter 8, which we begin by proving in a mostly manual way, invoking [crush] after each steop to discharge any low-hanging fruit. Our manual effort involves choosing which expressions to case-analyze on. *) (* begin hide *) Require Import MoreDep.