Questions tagged [isar]

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

Filter by
Sorted by
Tagged with
2 votes
1 answer
21 views

Picking this and calculation in Isabelle/JEdit output

This is a follow-up to How to write a low-level proof in Isar? Having ...
  • 207
1 vote
1 answer
46 views

How to write a low-level proof in Isar?

I would like to formalize ...
  • 207
8 votes
1 answer
167 views

Is there an elegant way of proving an equality A=B by going in both directions?

I would like to prove an equality by splitting it into a proof in each direction. Is there a more elegant style to start such a proof than this way:: ...
19 votes
2 answers
310 views

Why is Isabelle usually not just Isabelle but Isabelle/<xyz>?

For most proof assistants the name alone is common, E.g. Coq, Lean but with Isabelle it is often seen as Isabelle/<xyz>? Why the two parts? What is Isabelle/HOL Isabelle/FOL Isabelle/ZF ...
  • 2,796
7 votes
1 answer
107 views

Is there a way to use sledgehammer in Isar proofs?

I tried to use the sledgehammer command in Isabelle/HOL (2021) after the proof command, and got an error: Illegal application ...
  • 1,516