Email Gateway (Aug 19 2022 at 16:36): Email Gateway (Aug 19 2022 at 16:36):From: Ghassen HELALI <helali@encs.concordia.ca>
Hello fellows
I wonder to know if there is any way to port an old Isabelle/HOL code to a
the newest version of Isabelle.
The old code is dated from the year 2000
Regards
--gh
Email Gateway (Aug 19 2022 at 16:36):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi,
oh my dear, in which drawer has this been locked in all these years?
It is surely possible but will involve massive manual rephrasing. For a
more detailled statement a glimpse at the sources would be helpful.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 16:36):From: Lawrence Paulson <lp15@cam.ac.uk>
14-year-old code won’t be easy to port. A precise answer to your question depends very much on what this code does, how big it is, and what parts of Isabelle it uses.
Larry Paulson
Email Gateway (Aug 19 2022 at 16:36):From: "C. Diekmann" <diekmann@in.tum.de>
If it is actually no code (no ML) but primarily proof, you might be
(somewhat more) lucky. I see that there are afp entries dating back to
2003 [1], probably looking at their evolution could help (but this is
just a guess, ...).
Cornelius
[1] http://sourceforge.net/p/afp/afp-2003/ci/default/tree/thys/
Last updated: Nov 21 2024 at 12:39 UTC