Mercurial > cpdt > repo
comparison src/Large.v @ 445:0650420c127b
Finished vertical spacing
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Wed, 01 Aug 2012 17:31:56 -0400 |
| parents | 8077352044b2 |
| children | 980962258b49 |
comparison
equal
deleted
inserted
replaced
| 444:0d66f1a710b8 | 445:0650420c127b |
|---|---|
| 191 | 191 |
| 192 << | 192 << |
| 193 Error: Expects a disjunctive pattern with 3 branches. | 193 Error: Expects a disjunctive pattern with 3 branches. |
| 194 >> | 194 >> |
| 195 *) | 195 *) |
| 196 | |
| 197 Abort. | 196 Abort. |
| 198 | 197 |
| 199 (** Unsurprisingly, the old proof fails, because it explicitly says that there are two inductive cases. To update the script, we must, at a minimum, remember the order in which the inductive cases are generated, so that we can insert the new case in the appropriate place. Even then, it will be painful to add the case, because we cannot walk through proof steps interactively when they occur inside an explicit set of cases. *) | 198 (** Unsurprisingly, the old proof fails, because it explicitly says that there are two inductive cases. To update the script, we must, at a minimum, remember the order in which the inductive cases are generated, so that we can insert the new case in the appropriate place. Even then, it will be painful to add the case, because we cannot walk through proof steps interactively when they occur inside an explicit set of cases. *) |
| 200 | 199 |
| 201 Theorem eval_times : forall k e, | 200 Theorem eval_times : forall k e, |
| 560 Lemma slow' : forall x y, P x y -> Q x y -> S x y -> f x = f y. | 559 Lemma slow' : forall x y, P x y -> Q x y -> S x y -> f x = f y. |
| 561 Time eauto 6. | 560 Time eauto 6. |
| 562 (** << | 561 (** << |
| 563 Finished transaction in 2. secs (1.264079u,0.s) | 562 Finished transaction in 2. secs (1.264079u,0.s) |
| 564 >> | 563 >> |
| 565 | 564 %\vspace{-.15in}%Why has the search time gone up so much? The [info] command is not much help, since it only shows the result of search, not all of the paths that turned out to be worthless. *) |
| 566 Why has the search time gone up so much? The [info] command is not much help, since it only shows the result of search, not all of the paths that turned out to be worthless. *) | |
| 567 | 565 |
| 568 (* begin thide *) | 566 (* begin thide *) |
| 569 Restart. | 567 Restart. |
| 570 info eauto 6. | 568 info eauto 6. |
| 571 (** %\vspace{-.15in}%[[ | 569 (** %\vspace{-.15in}%[[ |