[isabelle-dev] HOL-ex

[Florian Haftmann]

> 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

Cheers,
	Florian

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