#2064 (Jun 18, 2020, 7:17:07 PM)

Mercurial (hg https://bitbucket.org/isa-afp/afp-devel/ default)

1. build bit operations on word on library theory on bit operations (detail)
2. more instances for uint types (detail)
3. canonical bit shifts for word type, leaving duplicates as they are at the moment (detail)
4. dropped yet another duplicate (detail)
5. replaced mere alias by input abbreviation (detail)
6. replaced mere alias by abbreviation (detail)
7. replaced operation with weak abstraction by input abbreviation (detail)
8. avoid compound operation (detail)
9. replaced mere alias by input abbreviation (detail)

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

1. more lemmas (detail / hgweb)
2. build bit operations on word on library theory on bit operations (detail / hgweb)
3. bit operations as distinctive library theory (detail / hgweb)
4. tweak for code generation (detail / hgweb)
5. pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all (detail / hgweb)
6. more lemmas and less name space pollution (detail / hgweb)
7. canonical bit shifts for word type, leaving duplicates as they are at the moment (detail / hgweb)
8. essential instance about bit structure (detail / hgweb)
9. more transfer rules (detail / hgweb)
10. dropped yet another duplicate (detail / hgweb)
11. fundamental construction of word type following existing transfer rules (detail / hgweb)
12. replaced mere alias by input abbreviation (detail / hgweb)
13. replaced mere alias by abbreviation (detail / hgweb)
14. replaced operation with weak abstraction by input abbreviation (detail / hgweb)
15. avoid compound operation (detail / hgweb)
16. formal relationships between operations (detail / hgweb)
17. eliminated warnings (detail / hgweb)
18. replaced mere alias by input abbreviation (detail / hgweb)

Started by an SCM change

This run spent:

• 2 min 0 sec waiting;
• 1 hr 11 min build duration;
• 1 hr 13 min total from scheduled to completion.