#1130 (Feb 25, 2020, 1:46:07 AM)

1. merged (detail / hgweb)
2. lift BNF witnesses for quotients (unless better ones are specified by the user) (detail / hgweb)
3. more robust (amending add9a9f6a290): proper syntax error instead of exception for grammar with unreachable nonterminals, e.g. nonterminal f1 syntax "_F" :: "f1 ⇒ 'b"  ("F _" 10); (detail / hgweb)
4. merged (detail / hgweb)
5. tuned var names (avoid h) (detail / hgweb)
6. more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1; (detail / hgweb)
7. a few new lemmas (detail / hgweb)

Started by an SCM change

This run spent:

• 56 min waiting;
• 1 hr 22 min build duration;
• 2 hr 18 min total from scheduled to completion.