[isabelle-dev] HOL-ex

[Lawrence Paulson]

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

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

I was hoping to get rid of it altogether. 

Larry