• Getting Started
  • Theories and Imports
• Technical
  • Versions

The best option to start working with Isabelle seems to be reading prog-prove.pdf and trying to solve as many of the exercises as possible.

Even though working with Isar (the proof abstraction language of Isabelle) feels mostly declarative, most mathematical definitions resemble a functional style. Therefore for those not already familiar with functional programming, a short introduction of its main concepts (like currying) and way of thinking may be beneficial.

Isabelle proof source files are called Theories. Theories can be grouped into Sessions.

A sort of minimal working example of a theory file is the following. Note that the file name needs to match the theory name or Isabelle will not run any code, so this example file must be named Example.thy.

theory Example
  imports Main
begin

end

Note that files missing an end will execute without warnings but cannot be imported, as Isabelle will complain about a Malformed theory.

Importing Main (a part of HOL) gives access to many classical mathematical definitions and results, including a.o. the natural numbers, sets, and lists. Complex_Main is an extension including the real numbers and beyond. In the absence of reasons against it, importing one of these is highly recommended as a baseline (see prog-prove.pdf).

For more information and advanced concepts see Sessions.

The simplest option for using Isabelle is to download a release version (see also past releases). Developers and early adopters can opt for nightly builds, or download and build the sources (see the official Mercurial repo or this more modern view).

Release versions do not receive patches, but are community tested with release candidates before going live (this then is the last chance to request features for a release). Release versions are scheduled to release every 8-10 months.

See also Isabelle NEWS and trends in 2020 (explained in talk:isa-news at ~1min), this comment on the Isabelle2021-1 release, and the section on Isabelle resources.