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

Lawrence Paulson 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 mailing list