eliminated obsolete var morphism;
simplified map_ctxt: just one version, without var;
removed obsolete params_of, prems_of, facts_of;
removed obsolete rename operations;
tuned;
Learning and using Isabelle
tutorial Tutorial on Isabelle/HOL
isar-overview Tutorial on Isar
locales Tutorial on Locales
classes Tutorial on Type Classes
functions Tutorial on Function Definitions
codegen Tutorial on Code Generation
sugar LaTeX sugar for proof documents
ind-defs (Co)Inductive Definitions in ZF
Reference Manuals
isar-ref The Isabelle/Isar Reference Manual
implementation The Isabelle/Isar Implementation Manual
system The Isabelle System Manual
ref The Isabelle Reference Manual
logics Isabelle's Logics: overview and misc logics
logics-HOL Isabelle's Logics: HOL
logics-ZF Isabelle's Logics: FOL and ZF