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