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

[Lawrence Paulson]

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

> On 30 Jan 2022, at 12:18, Makarius <makarius at sketis.net> wrote:
> 
> Here I have taken into account that ancient Isabelle lore did not transmit if "ex" means "examples" are "experiments".