* @{lemma} in latex and ML: allow initial and terminal method expressions, as in the Isar command 'by'. * @{lemma} in ML now closes the derivation, unless @{lemma (open) ...} is specified.