All Questions
5 questions
2
votes
2
answers
132
views
What is an assumption in Isar?
I have the following code:
lemma assumes "A" shows "A ∧ A"
proof -
show "A ∧ A"
apply (rule conjI)
apply assumption
Now, ...
- 323
0
votes
0
answers
39
views
Simple and proper methods in Isar
https://isabelle.systems/cookbook/src/proofs/methods/Chained_Facts.thy
talks about
We note a slight difference. In the variant with intro, a trivial goal remains
that we need to solve by ‹assumption›....
- 323
3
votes
1
answer
36
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
...
- 323
19
votes
2
answers
436
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,856
7
votes
1
answer
264
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 ...
- 2,662