I do remember. It’s almost a shame how years of work can be executed in minutes. Larry
> On 15 Jan 2016, at 19:16, Makarius <makar...@sketis.net> wrote: > > The sessions from Bali to JinjaThreads are historically related; this used to > be the top-end in resource usage until 1-2 years ago. About 12 years ago, > MicroJava was in the range of 1h. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev