> 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. > All old/misc/test material would remain in HOL-ex? I was hoping to get rid of it altogether. Larry _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
