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.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
