conversion

Stream: general

[Michael Beeson]

How can I use the conversion tactic mode to rewrite at a specific location in a hypothesis? As in rw h33 at h35,
but at a specific location as can be done in the goal by conv begin ... end.

[Kevin Buzzard]

What happens if you try conv ... at h35?

[Michael Beeson]

I'll try that, thanks. I put the "at" after the rw and that didn't work, I didn't think of putting it after "conv". The manual is dead silent on this point.