Email Gateway (Aug 18 2022 at 12:59): Email Gateway (Aug 18 2022 at 12:59):From: "\"Juan Rodriguez Hortalá\"" <juanrh@fdi.ucm.es>
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
Email Gateway (Aug 18 2022 at 12:59):From: Gergely Buday <gbuday@gmail.com>
Juan Rodriguez Hortalá wrote:
This thread might be of interest to you:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2009-January/msg00035.html
Email Gateway (Aug 18 2022 at 13:00):From: Tobias Nipkow <nipkow@in.tum.de>
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.
Tobias
Juan Rodriguez Hortalá schrieb:
Email Gateway (Aug 18 2022 at 13:00):From: "\"Juan Rodriguez Hortalá\"" <juanrh@fdi.ucm.es>
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@in.tum.de>
Fecha: Domingo, Febrero 15, 2009 12:08
Asunto: Re: [isabelle] Isar tutorial and legacy warnings
A: Juan Rodriguez Hortalá <juanrh@fdi.ucm.es>
CC: isabelle-users@cl.cam.ac.uk
Last updated: May 03 2024 at 08:18 UTC