Re: [isabelle] “Programming in Isabelle/HOL”

On 02/19/2014 12:23 AM, Yannick Duchêne (Hibou57) wrote:
Unless I missed it, this one is not listed on

A single concise and comprehensive page on a kind of wiki:

uuups, feeling repsonsible for that page I wouldn't recommend it as a "concise and comprehensive" introduction to “Programming in Isabelle/HOL”.

That page collected ad-hoc notes from the work with some students in mathematics, who were neither good in programming nor really interested in computer theorem proving.

For the next group of students this page will undergo essential updates --- for compelling reasons!

May be useful to keep close at hands, as an example to mention it within replies to people who ask questions on StackOverflow about SML programming and someone invite him/her to try SML from Isabelle, as I've noticed this sometimes occurs.

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