Isabelle, which is available from http://isabelle.in.tum.de , is a generic framework for interactive theorem proving. The Isabelle/Puremeta-logic allows the formalization of the syntax and inference rules of a broad range of object-logics following the general idea of natural deduction [32,33]. The logical core is implemented according to the well-known "LCF approach" of secure inferences as abstract datatype constructors in ML [16]; explicit proof terms are also available [8]. Isabelle/Isarprovides sophisticated extra-logical infrastructure supporting structured proofs and specifications, including concepts for modular theory development. Isabelle/HOLis a large application within the generic framework, with plenty of logic-specific add-on tools and a large theory library. Other notable object-logics are Isabelle/ZF(Zermelo-Fraenkel set-theory, see [34,36] and Isabelle/HOLCF[26] (Scott's domain theory within HOL). Users can build further formal-methods tools on top, e.g. see [53].