Re: [isabelle] A (very) short Isabelle/HOL tutorial for the functional programmer
On Mon, Oct 19, 2015 at 7:01 PM, Makarius <makarius at sketis.net> wrote:
> On Mon, 19 Oct 2015, Thomas Genet wrote:
> I wrote a 4 pages Isabelle/HOL tutorial for the functional programmer. It
>> is available here:
>> Any feedback and comments are welcome.
The text reads a bit like a "script" for an interactive session, conducted
> by the user or the presenter of a quick tutorial. It would be nice to see
> online videos like that.
When I reach there I'll make one :-) But for now...
For me it is always interesting to see what needs to be explained on first
Programmers need a "Hello World" example to get off the ground.
Until I saw Thomas' example I could not understand that (or rather how)
Isabelle hops between define-mode (eg fun/primrec etc) and prove-mode
This archive was generated by a fusion of
Pipermail (Mailman edition) and