[isabelle-dev] HOL-ex

[Makarius]

On 04/06/2020 11:42, Lawrence Paulson wrote:
>> On 3 Jun 2020, at 20:30, Makarius <makarius at sketis.net> 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