Intuitionistic higher-order logic — the fragment comtaining implication, universal quantification, and equality — can serve as a meta-logic for formalizing various logics. As an example, axioms formalizing first-order logic are presented, and proved sound and complete by induction on proof trees. Proofs in higher-order logic represent derivations of rules as well as proofs of theorems. A proof develops by deriving rules using higher-order resolutions. The discharge of assumptions involves derived meta-rules for ‘lifting’ a proposition. Quantifiers require a similar lifting rule or else Hilbert’s ε-operator. The alternatives are contrasted through several examples. Hilbert’s ε underlies Isabelle’s original treatment of quantifiers, but the lifting rule is logically simpler. The meta-logic is used in the latest version of the theorem prover Isabelle. It extends the logic used in earlier versions. Compared with other meta-logics, higher-order logic has a weaker type system but seems easier to implement.