moved theorem tags from Drule to PureThy;
replaced kind attribute by kind string;
tuned name_multi: index > 1 only;
added note_thmss_qualified (from Isar/locale.ML);
Learning Isabelle
tutorial Tutorial on Isabelle/HOL
isar-overview Tutorial on Isar
locales Tutorial on Locales
Reference Manuals
isar-ref The Isabelle/Isar Reference Manual
implementation The Isabelle/Isar Implementation
system The Isabelle System Manual
ref The Isabelle Reference Manual
Logics
logics Isabelle's Logics: overview and misc logics
logics-HOL Isabelle's Logics: HOL
logics-ZF Isabelle's Logics: FOL and ZF
Specific Topics
sugar LaTeX sugar for proof documents
axclass Tutorial on Axiomatic Type Classes
ind-defs (Co)Inductive Definitions in ZF