Show the use of reflection attribute; fixed comments about the order of absorbing equations : f (C x) = x ; now automaically tried as last;
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
axclass Tutorial on Axiomatic Type Classes
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
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