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

Makarius 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 mailing list