TableFun.join/merge: optimize the important special case where the tables coincide -- NOTE: this changes both the operational behaviour and the result for non-standard join/eq notion;
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
Reference Manuals
isar-ref The Isabelle/Isar Reference Manual
implementation The Isabelle/Isar Implementation Manual
system The Isabelle System Manual
Old Manuals (outdated!)
intro Old Introduction to Isabelle
ref Old 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
ind-defs (Co)Inductive Definitions in ZF