[isabelle] Isar tutorial and legacy warnings



Hi, I'm using the tutorial for Isar from http://isabelle.in.tum.de/dist/Isabelle/doc/isar-overview.pdf 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 fdi.ucm.es
Home Page: http://gpd.sip.ucm.es/juanrh/
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.