We survey results about several proof systems for intuitionistic logic, beginning with a paper by Vorob’ev and including work of Hudelmaier and Herbelin. All have the property that, in our notation, there are two kinds of sequent, in one of which the formula in a special place, here called the focus, is the only possibility for use as principal formula. Inter alia we present some strengthenings of classical (but not well-known) results and an application to Jankov’s logic of weak excluded middle, complementing by proof-theoretic methods results of Fiorino et al in Milan.