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