[isabelle-dev] HOL/Examples vs HOL/ex
makarius at sketis.net
Sun Jan 30 13:18:29 CET 2022
On 30/01/2022 13:07, Lawrence Paulson wrote:
> It’s confusing that we have these two examples directories. Isn’t it time they were amalgamated, and perhaps some of the material moved elsewhere?
Since Isabelle2021-1 we actually have 4, with the following names and
descriptions (in the session ROOT):
Pure-Examples -- Notable Examples for Isabelle/Pure.
Pure-ex -- Miscellaneous examples and experiments for Isabelle/Pure.
HOL-Examples -- Notable Examples for Isabelle/HOL.
HOL-ex -- Miscellaneous examples and experiments for Isabelle/HOL.
Here I have taken into account that ancient Isabelle lore did not transmit if
"ex" means "examples" are "experiments".
We can certainly consolidate this further by promoting a few more
"miscellaneous examples" to "notable examples": by moving them and putting
them into proper shape.
We do need a bin for "miscellaneous examples and experiments", and I think the
traditional "ex" directories are a good place for that.
More information about the isabelle-dev