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

[Makarius]

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