The Isabelle reference manual
Lawrence Charles Paulson · 2021
This manual is a comprehensive description of Isabelle, including all commands, functions and packages. It is intended for reference rather than for reading through, and is certainly not a tutorial. The manual assumes familiarity with the basic concepts explained in Introduction to Isabelle. Functions are organized by their purpose, by their operands (subgoals, tactics, theorems), and by their usefulness. In each section, basic functions appear first, then advanced functions, and finally esoteric functions.