- afp: The Archive of Formal Proofs is a collection of proof libraries, examples, and larger scientific developments.
- isafol: The Isabelle Formalization of Logic covers logical calculi (e.g. CDCL and resolution) and related topics.
- isafor: The Isabelle Formalization of Rewriting covers abstract rewriting and first-order term rewriting.
- isarmathlib: Formalised mathematics for Isabelle/ZF.
- standard: The standard library included in Isabelle