lp15 at cam.ac.uk
Thu Jun 4 11:42:37 CEST 2020
> 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,
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.
More information about the isabelle-dev