Commit 2c49c95d authored by Adam Chlipala's avatar Adam Chlipala

Pass through Chapter 2

parent 545d7fb8
...@@ -401,6 +401,12 @@ app_assoc_reverse ...@@ -401,6 +401,12 @@ app_assoc_reverse
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: *) 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 ((_ ++ _) ++ _). SearchRewrite ((_ ++ _) ++ _).
(** %\vspace{-.15in}%[[ (** %\vspace{-.15in}%[[
app_assoc_reverse: app_assoc_reverse:
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment