[isabelle-dev] HOL/Examples vs HOL/ex
lp15 at cam.ac.uk
Sun Jan 30 13:30:07 CET 2022
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.
> 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".
More information about the isabelle-dev