Commit 0b421721 authored by Adam Chlipala's avatar Adam Chlipala

Small prose change

parent e70a599d
...@@ -391,7 +391,7 @@ We start out the same way as before, introducing new free variables and unfoldin ...@@ -391,7 +391,7 @@ We start out the same way as before, introducing new free variables and unfoldin
unfold expDenote. unfold expDenote.
fold expDenote. fold expDenote.
(** Now we arrive at a point where the tactics we have seen so far are insufficient: (** Now we arrive at a point where the tactics we have seen so far are insufficient. No further definition unfoldings get us anywhere, so we will need to try something different.
[[ [[
......
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