Re: [isabelle] Isar tutorial and legacy warnings



Juan Rodriguez Hortalá wrote:

> lemma l1 : "A --> A"
> proof
>  assume "A"
>  show "A" .
> qed
>
> So I would like to ask the list for some tutorial and documentation for Isabelle 2008, that could be free of legacy warnings.

This thread might be of interest to you:

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2009-January/msg00035.html

- Gergely





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