#5235 (Apr 21, 2024, 12:41:07 PM)

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

1. merged (detail)
2. feat(Transport) add simpler function type introduction rule for extend (detail)
3. feat(Transport) functions as binary relations, improved mono notation, make non-dependent relators definitions, generalise some concepts (detail)
4. feat(ML_Unificaiton) repeated resolution tactics, tactics now proving theorems up to alpha (and not alpha-eta) equivalence, fix wrong bounded variables substitution (detail)

Started by an SCM change

This run spent:

• 2 min 4 sec waiting;
• 18 min build duration;
• 21 min total from scheduled to completion.