[isabelle-dev] HOL-ex

Tobias Nipkow nipkow at in.tum.de
Thu Jun 4 10:24:44 CEST 2020

On 03/06/2020 21:30, Makarius wrote:
>>> On 31 May 2020, at 22:52, Makarius <makarius at sketis.net> wrote:
>>>> 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.
> On 01/06/2020 10:48, Lawrence Paulson wrote:
>> I was definitely not proposing subdirectories of ex. Rather I was proposing multiple directories, if there are enough related items to make a meaningful collection.
> So you were proposing multiple sessions, like we have already with HOL-Induct,
> HOL-Isar_Examples?


> Would it mean to have another one, lets say HOL-Examples with sufficiently
> interesting and up-to-date examples?

I would merge it with Isar_Examples.

> All old/misc/test material would remain in HOL-ex?

For the time being, yes.


> 	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5579 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20200604/77b2b2c1/attachment.bin>

More information about the isabelle-dev mailing list