Isabelle, which is available from http://isabelle.in.tum.de, is a generic framework for interactive theorem proving. The Isabelle/Pure meta-logic allows the formalization of the syntax and inference rules of a broad range of object-logics fol- lowing 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/Isar pro- vides sophisticated extra-logical infrastructure supporting structured proofs and speci- fications, including concepts for modular theory development. Isabelle/HOL is 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). Beginners are advised to start working with Isabelle/HOL; see the tutorial volume (30), and the companion tutorial (28) covering structured proofs. A general impression of Isabelle/HOL and ZF compared to other systems like Coq, PVS, Mizar etc. is given in (52). The Proof General Emacs interface (3) is still the de-facto standard for interaction with Isabelle. The Isabelle document preparation system enables one to generate high- quality PDF-LAT E X documents from the original theory sources, with full checking of the formal content. The Archive of Formal Proofs http://afp.sf.net collects proof libraries, ex- amples, and larger scientific developments, mechanically checked with Isabelle. AFP is organized like a journal everybody can contribute to. Submitting formal theories there helps to maintain applications in the longer term, synchronized with the ongoing devel- opment of Isabelle itself.