Delete trailing whitespace in help/Docfiles

docs for changes to irule and functions it uses

GEN_VALIDATE(_LT) - flag for adding new subgoals in any event

GEN_VALIDATE false is like VALIDATE, but adds subgoals for the assumptions
of the theorem produced by the justification, regardless of whether they
are among the assumptions of the goal. Advantage of this is that
GEN_VALIDATE false (ACCEPT_TAC th) produces predictable subgoals,
which may help in coding compound tactics

VALIDATE and VALIDATE_LT

If tac (ltac) is invalid due to proving theorems with extra assumptions,
VALIDATE tac and VALIDATE_LT ltac make the tactic valid by returning extra
subgoals to prove the extra assumptions