Mercurial > cpdt > repo

comparison src/StackMachine.v @ 492:fa2eb72446a8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pass through Chapter 2
author Adam Chlipala <adam@chlipala.net>
date Fri, 18 Jan 2013 14:22:50 -0500
parents 1fd4109f7b31
children a4b3386ae140
comparison
equal deleted inserted replaced
491:da576746c3ba 492:fa2eb72446a8
398 : forall (A : Type) (l m n : list A), (l ++ m) ++ n = l ++ m ++ n 398 : forall (A : Type) (l m n : list A), (l ++ m) ++ n = l ++ m ++ n
399 399
400 ]] 400 ]]
401 401
402 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: *) 402 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: *)
403
404 (* begin hide *)
405 (* begin thide *)
406 Definition bleh := app_assoc.
407 (* end thide *)
408 (* end hide *)
403 409
404 SearchRewrite ((_ ++ _) ++ _). 410 SearchRewrite ((_ ++ _) ++ _).
405 (** %\vspace{-.15in}%[[ 411 (** %\vspace{-.15in}%[[
406 app_assoc_reverse: 412 app_assoc_reverse:
407 forall (A : Type) (l m n : list A), (l ++ m) ++ n = l ++ m ++ n 413 forall (A : Type) (l m n : list A), (l ++ m) ++ n = l ++ m ++ n