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

Makarius 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 mailing list