[isabelle-dev] HOL/Examples vs HOL/ex
makarius at sketis.net
Sun Jan 30 14:53:14 CET 2022
On 30/01/2022 13:30, Lawrence Paulson wrote:
> I certainly intended it to abbreviate “examples”.
Yes, I vaguely remember that. Later, people (including myself) added genuine
> 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.
I see two possibilities here without regression of the state-of-the-art:
(1) move it to AFP
(2) move it to HOL-Examples
More information about the isabelle-dev