Email Gateway (Mar 27 2025 at 17:05): Email Gateway (Mar 27 2025 at 17:05):From: Gunnar Teege <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
after quite a long time I just published a new update to my gentle
introduction to Isabelle and Isabelle/HOL. As before, it is a available at
https://github.com/gteege/gentle-isabelle/blob/main/man-isabelle.pdf?raw=true
A version with changebars relative to the previous version of July, 20,
2024 is available at
https://github.com/gteege/gentle-isabelle/blob/main/man-isabelle-changes.pdf?raw=true
The main additions are new sections about bounded natural functors
(BNF), quotient types, and the mechanisms for transfer and lifting.
Together they are an important underpinning for defining types in HOL.
There are also several minor improvements and some corrections. Finally,
I updated the document according to the new Isabelle release 2025.
Comments and problem reports are welcome. Enjoy.
Gunnar Teege
Last updated: Apr 17 2025 at 20:22 UTC