Skip to main content

Use this tag for the ISAR (Intelligible semi-automated reasoning) proof language in the Isabelle proof assistant.

Isar (Intelligible semi-automated reasoning) is the main proof language of the Isabelle proof assistant. Inspired by the Mizar system, Isar is designed for writing readable structured proofs, as compared to old style apply-scripts in Isabelle.