Re: [isabelle] Isar tutorial and legacy warnings

Those proofs indeed no loger work in the development version. There you
also find an updated Tutorial. Note however, that the proofs in the
updated Tutorial were merely locally patched - as a result the tutorial
is a bit inelegant in those places.


Juan Rodriguez Hortalá schrieb:
> Hi, I'm using the tutorial for Isar from that I've found under the section "Tutorials, Manuals and Library Theories for Isabelle2008". But when trying the examples in Isabelle 2008 I get "Legacy feature" warnings all the time, in proofs as simple as:
> 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.
> Greetings,
> Juan
>  -- 
> ------------------------------------------------------------------------
> Juan Rodríguez Hortalá
> Grupo de Programación Declarativa / Declarative Programming Group
> E-Mail : juanrh at
> Home Page:
> Tel: + 34 913947646
> Despacho / Office: 220 (2ª planta / 2nd floor)
> Dept. Sistemas Informáticos y Computación / Department of Computer Systems and Computing
> Universidad Complutense de Madrid
> Facultad de Informática
> C/ Profesor José García Santesmases, s/n
> E - 28040 Madrid. Spain

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