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. Maybe feed should also be adjusted to be written feed H using tac? Actually 'using' is a strange verb here, it sounds like tac is involved in the feeding, but that's not the case. Is to a keyword already, i.e., can we use efeed H to tac? Or into?

See also the discussion here: !389 (comment 82750)

@robbertkrebbers Please feel free to update this MR as you see fit.