search

lawrencecpaulson / lawrencecpaulson.github.io

the blog "Machine Logic"
12 stars 0 forks source link

https://lawrencecpaulson.github.io/2022/05/11/jEdit-tricks.html #14

Open utterances-bot opened 2 years ago

utterances-bot commented 2 years ago

9. Getting started: basic Isabelle/jEdit tricks

https://lawrencecpaulson.github.io/2022/05/11/jEdit-tricks.html

sterraf commented 2 years ago

I recall crystal-clearly from my first experiences being puzzled after proving "False" without any error message (the same way as above). Even more so, if the "whoops" lemma were in a different theory file. So this post is a great piece of advice!

Another thing that was very intriguing, again while transitioning from apply-style scripts to Isar structured proofs, was the cryptic status line indicating "Proof(prove)" and "Proof(state)". I tried to make that simple in two comments on Proof Assistants SE.