#2034 (Aug 12, 2022, 1:33:12 AM)

Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

1. removing the [simp] attribute breaks too many AFP entries severely (detail)
2. nlists is picked up automatically but conflicts with the RBT setup (detail)
3. new lemma (detail)
4. merged (detail)
5. New theory of fixed length lists (detail)

Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

1. adapted to NLists.thy (detail)
2. merged (detail)
3. use Library/NList.thy now (detail)

Started by an SCM change

This run spent:

• 8.8 sec waiting;
• 11 hr build duration;
• 11 hr total from scheduled to completion.