Refactor and improve documentation of feed and efeed tactics
This MR is based on !389 (closed).
Discussion from !389 (comment 82974) :
The documentation does not even mention the
by
part of this tactic. Also,efeed tac H
(which is what the documentation uses in the first line) is not the correct syntax for this tactic. Maybefeed
should also be adjusted to be writtenfeed H using tac
? Actually 'using' is a strange verb here, it sounds liketac
is involved in the feeding, but that's not the case. Isto
a keyword already, i.e., can we useefeed H to tac
? Orinto
?
See also the discussion here: !389 (comment 82750)
@robbertkrebbers Please feel free to update this MR as you see fit.
Edited by Michael Sammler