Sort search results in order of relevance, where relevance =
a) better if 0 premises for intro or 1 premise for elim/dest rules
b) better if substitution size wrt to current goal is smaller
Only applies to intro, dest, elim, and simp
(contributed by Rafal Kolanski, NICTA)
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
ref The Isabelle Reference Manual
system The Isabelle System 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