On 04/06/2020 11:42, Lawrence Paulson wrote:
>> On 3 Jun 2020, at 20:30, Makarius <[email protected]> wrote:
>>
>> So you were proposing multiple sessions, like we have already with
>> HOL-Induct,
>> HOL-Isar_Examples?
>
> I don’t understand this point. For both HOL-Induct and HOL-Isar_Examples
> there is a relatively small directory with a single session.
>
>> Would it mean to have another one, lets say HOL-Examples with sufficiently
>> interesting and up-to-date examples?
>
> I would say that some reorganisation is needed. Certainly any regression
> testing material belongs elsewhere.
Strictly speaking, we don't have regression testing material, just "examples".
Some are for users to look at, some are for tools to crunch, some are both.
>> All old/misc/test material would remain in HOL-ex?
>
> I was hoping to get rid of it altogether.
HOL-ex has always been an odd bin for very mixed material. I don't see a
reason to delete that: otherwise we would have to question other odd sessions,
too.
We could rather leave HOL-ex as is, and move some of the better examples into
a new session HOL-Examples (with material from other sessions, like
HOL-Isar_Examples).
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
