[isabelle-dev] HOL-ex

[Makarius]

On 31/05/2020 21:19, Lawrence Paulson wrote:
> Tobias has pointed out that directory ex is easily overlooked these days and perhaps we should rename it, e.g. to Examples. Any comments? 

That directory is a rather ancient Isabelle tradition, but already 10-15 years
ago, it has declined in relevance: most examples are rather odd experiments,
so "ex" could just as well mean that.

We could think of genuine examples in a new HOL-Examples session, without 90%
of the odd stuff. But this would also mean to reform sessions like
HOL-Isar_Examples in a similar manner.

In the past 10 years, I have de-facto used the "Examples" slot of the
Isabelle/jEdit Documentation panel to refer to other sessions with examples.


> Conceivably it could be subdivided, as it seems to have 94 entries.

Now might be actually a good time to disallow sub-directories of a session
directory. They have accumulated a lot of confusion and problems in the past
decades.

See also my NEWS reading on the Isabelle 2020 Workshop:

https://files.sketis.net/Isabelle_Workshop_2020/Isabelle_2020_paper_7.pdf

"""
As a future clarification of the session structure, session sub-directories
could be
superseded by “tags” to group theories via “topics”. Thus the space of session-
qualified theories would directly correspond to the file-system arrangement, with-
out the potential confusion via duplicates in different sub-directories. The
Prover
IDE would present tags via a suitable GUI presentation, e.g. a “tag cloud” instead
of an old-fashioned directory tree.
"""


	Makarius