Isabelle is a generic theorem prover. Object-logics are formalized within higher-order logic, which is Isabelle's meta-logic. Proofs are performed by a generalization of resolution, using higher-order uniflcation. The latest incarnation of Isabelle, Isabelle-91, features a type system based on order-sorted uniflcation; this supports polymorphism and overload- ing in logic deflnitions.