Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] HOL/Examples vs HOL/ex


view this post on Zulip 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

view this post on Zulip 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 07 2024 at 16:22 UTC