[isabelle-dev] HOL-ex

[Makarius]

>> 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?

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


	Makarius