intro Introduction to Isabelle ref The Isabelle Reference Manual system The Isabelle System Manual logics Isabelle's Object-Logics ind-defs (Co)Inductive Definitions in ZF axclass Tutorial on Axiomatic Type Classes