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

[Makarius]

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