Re: [isabelle] Isar tutorial and legacy warnings



Hi, the tutorials in http://isabelle.in.tum.de/devel/Isabelle_04-Feb-2009_pdf.tar.gz are what I was looking for, thank you.

Greetings,

Juan

----- Mensaje original -----
De: Tobias Nipkow <nipkow at in.tum.de>
Fecha: Domingo, Febrero 15, 2009 12:08
Asunto: Re: [isabelle] Isar tutorial and legacy warnings
A: Juan Rodriguez Hortalá <juanrh at fdi.ucm.es>
CC: isabelle-users at cl.cam.ac.uk

> 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 
> tutorialis a bit inelegant in those places.
> 
> Tobias
> 
> Juan Rodriguez Hortalá schrieb:
> > 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
> > 
> 
> 

 -- 
------------------------------------------------------------------------
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.