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 <[email protected]> wrote: > > Here I have taken into account that ancient Isabelle lore did not transmit if > "ex" means "examples" are "experiments". _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
