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

Le Wed, 19 Feb 2014 14:39:59 +0100, Walther Neuper <wneuper at> a écrit:
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,
This was looking good ad‑hoc introductory notes to a seasoned like me. I guess if you're teacher, you know better than I do, so as your appreciation on this page is not so good, I will avoid posting it in other places (unfortunately, I already posted it on StackOverflow yesterday, in a comment).

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!

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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