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
experiments.
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
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
