Email Gateway (Jan 30 2022 at 12:07): Email Gateway (Jan 30 2022 at 12:07):From: Lawrence Paulson <lp15@cam.ac.uk>
It’s confusing that we have these two examples directories. Isn’t it time they were amalgamated, and perhaps some of the material moved elsewhere?
Larry
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Jan 30 2022 at 12:30):From: Lawrence Paulson <lp15@cam.ac.uk>
I certainly intended it to abbreviate “examples”.
There are a few things (e.g. the proof that Ackermann’s function isn’t primitive recursive) that perhaps belong in the AFP, and are almost invisible in HOL/ex.
Larry
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Dec 21 2024 at 16:20 UTC