[isabelle-dev] HOL-ex

[Makarius]

On 02/06/2020 07:55, Florian Haftmann 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? Conceivably it could be subdivided, as it seems to have 94 entries.
> 
> I'm skeptic that there is enough related material to carve out distinct
> thematically grouped sessions.
> 
> IMHO there is one central observation: HOL-ex consists of
> a) genuine examples apt for studying
> b) rather technical matter (e.g. testings simprocs etc.) and idea sketches
> 
> a) could go to Isar examples
> b) could maybe be distributed to corresponding sessions

This proposal for a) sounds like renaming HOL-Isar_Examples to HOL-Examples,
adding a few things from HOL-ex, and maybe (re)moving a few old things from
it. (Note that historically, HOL-Isar_Examples is from a time, when almost
everything else was non-Isar --- hard to believe today.)


The proposal for b) is similar to what I suggested earlier: HOL-Library in
particular would absorbs a few more genuine examples, e.g. HOL-ex.SOS as
HOL-Library.Sum_of_Squares_Examples.

In the past that was considered a problem, because the underlying image would
become a bit slower and bigger. Now we have fewer uses of HOL-Library as
parent image, instead the few required theories are included/reloaded via
"'sessions' HOL-Library".


	Makarius

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20200603/dd4ed7d8/attachment-0001.sig>