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:

- Gergely

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