Re: [isabelle] Isabelle guide for mathematicians



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.