repeat the given instruction until it ``fails''
The given instruction is run repeatedly until it ``fails''. A call of
:repeat always ``succeeds''.
Remark: There is nothing here in general to prevent the instruction
from being run after all goals have been proved, though it may then fail, thus
causing :repeat to return.