Mercurial > cpdt > repo
changeset 492:fa2eb72446a8
Pass through Chapter 2
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Fri, 18 Jan 2013 14:22:50 -0500 |
parents | da576746c3ba |
children | 4a663981b699 |
files | src/StackMachine.v |
diffstat | 1 files changed, 6 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/src/StackMachine.v Fri Jan 18 13:45:00 2013 -0500 +++ b/src/StackMachine.v Fri Jan 18 14:22:50 2013 -0500 @@ -401,6 +401,12 @@ If we did not already know the name of the theorem, we could use the %\index{Vernacular commands!SearchRewrite}%[SearchRewrite] command to find it, based on a pattern that we would like to rewrite: *) +(* begin hide *) +(* begin thide *) +Definition bleh := app_assoc. +(* end thide *) +(* end hide *) + SearchRewrite ((_ ++ _) ++ _). (** %\vspace{-.15in}%[[ app_assoc_reverse: