Email Gateway (Mar 25 2024 at 13:08): Email Gateway (Mar 25 2024 at 13:08):From: 伊藤洋介 <glacier345@gmail.com>
Dear Gunnar Teege,
Thank you for sharing the tutorial.
This is very helpful for me, and presumably for beginners.
I will let you know if I find any errors.
Best regards,
2024年3月25日(月) 18:27 Gunnar Teege <gunnar.teege@unibw.de>:
Email Gateway (Mar 25 2024 at 15:50):From: Gunnar Teege <gunnar.teege@unibw.de>
Dear Isabelle Community,
when I started to use Isabelle some years ago I had no background in
formal proof systems other than a basic knowledge of mathematical
logics. I found it very challenging to understand what the system does
and how it is used. The extensive documentation (which I appreciate a
lot in the meantime) was of limited help at the beginning: it is spread
across several documents and it is either oriented towards specific
applications (the tutorials about program semantics) or requires
profound knowledge of proof systems for understanding (the reference
manual etc). It did not provide the orientation I needed for a thorough
insight into the language used to write theories and proofs.
At some point I started to turn my notes into a document to help my
students and research assistants with this task. It became much larger
than expected, but it was perceived to be helpful. Then I decided that
it may be useful for others as well, if it covers a substantial part of
Isabelle and Isabelle/HOL. So I revised and extended it, while having
fun in exploring the features of Isabelle and Isabelle/HOL, and it again
became much larger than intended.
Here I share the current state of the document. There are still some
parts missing and many possible improvements, but it should already give
an impression about what it intends to be. If you like it I will
contribute it to the Isabelle community and extend and maintain it
according to my capacities. Perhaps it can be helpful in further
enlarging the community of Isabelle users.
Of course I appreciate all kinds of feedback, in particular, if you note
errors, misconceptions or over-simplifications. And no, I do not expect
that you proof-read a 200 pages document. Just get an impression.
Best regards
Gunnar Teege
Last updated: Apr 28 2024 at 16:17 UTC