On 03/06/2020 21:30, Makarius wrote:
On 31 May 2020, at 22:52, Makarius <[email protected]> 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?
Yes.
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. Tobias
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
