Email Gateway (Aug 22 2022 at 15:01): Email Gateway (Aug 22 2022 at 15:01):From: Makarius <makarius@sketis.net>
On 06/02/17 00:38, Alexander Hicks wrote:
Attached is a short guide intended to introduce Isabelle to mathematicians
or more generally people with a mathematical rather than computer science
background.
I always find it interesting to see how mathematicians understand our
proof system. It definitely influences its future evolution.
I think we would also both be fine with someone building on top of this
if they wish, we still have the tex file.
Just looking at the PDF it was obvious to me that this is an informal
(La)TeX document, the way how mathematicians like to do it.
Did you know that Isabelle is first and foremost a formal document
preparation system, with LaTeX merely as backend for low-level
typesetting? See the explanation of "isabelle mkroot -d" in the "system"
manual.
Using Isabelle sources for a document like yours makes it easy to quote
formal pieces. either checked or unchecked (e.g. via the @{text} and
@{theory_text} antiquotations). It also makes it easier to keep the
document up-to-date wrt. inevitable changes of Isabelle.
Makarius
Email Gateway (Aug 22 2022 at 15:05):From: Alexander Hicks <alexanderlhicks@gmail.com>
Hello everyone,
Attached is a short guide intended to introduce Isabelle to mathematicians
or more generally people with a mathematical rather than computer science
background. The guide was written by myself (Alexander Hicks) and José
Siqueira (CC'd). Both of us completed an MASt in Mathematics at Cambridge
and worked with Isabelle over the summer at the Cambridge Computer
Laboratory. We decided to write this guide as the existing content we found
was mostly written by and geared towards computer scientists.
I've attached a pdf copy of the guide, I've also uploaded it to a github
page: https://github.com/alexanderlhicks/IsabelleGuide so there is a
permanent link to it. Feel free to host it and distribute it as you like.
Hopefully so of you will find it useful or interesting.
Note that neither José or I are currently (or will be in the near future)
doing work related to Isabelle so there are no current plans to keep this
updated with new Isabelle releases and so on. If you find mistakes or have
comments, we will both be happy to amend the current version as time allows
(so it could take a while). I think we would also both be fine with someone
building on top of this if they wish, we still have the tex file.
Cheers,
Alex
Isabelle_Guide.pdf
Last updated: Nov 21 2024 at 12:39 UTC