Email Gateway (Aug 18 2022 at 15:35): Email Gateway (Aug 18 2022 at 15:35):From: grechukbogdan <grechukbogdan@yandex.ru>
Dear Isabelle Users
Thank you everyone who provided me with a feedback for this document.
I took into account all the suggestions and corrections, and the new version of the document is attached.
I plan to wait about two-three more weeks in case if someone would have more global suggestions, and then I plan to find someone to help me with polishing English.
I really hope such a Primer will be helpfull for beginners.
Sincerely,
Bogdan
document.tex
document.pdf
Email Gateway (Aug 18 2022 at 15:44):From: grechukbogdan <grechukbogdan@yandex.ru>
Dear Isabelle Users
I have tried to write a short Primer aimed for mathematicians who would like to use Isabelle first time for formalization of mathematical results, but do not want to read a 218-page tutorial before formalizing the first simple lemma.
I have tried to concentrate on topics, which are especially useful for a beginner: main notations, search in Isabelle, sledgehammer, organization of blocks inside the proof, etc. More importantly, I have tried not just tell the reader ``how it works'', but tell how to learn Isabelle, looking at the existing theories. Also, instead of providing the reader with correct proofs immediately, I often start with intuitive, but incorrect versions, and describe how to correct the resulting errors.
The current version of the Primer is attached.
Any feedback would be appreciated.
Sincerely,
Bogdan.
document.tex
Last updated: Nov 21 2024 at 12:39 UTC