#1378 (Jan 2, 2018, 9:28:18 PM)

1. old_datatype no longer exists (cf. 706b1cf7b76d); (detail / hgweb)
2. merged (detail / hgweb)
3. PIDE markup for Markdown items (which may consist of multiple paragraphs or lists); (detail / hgweb)
4. clarified terminology of "markdown_bullet"; (detail / hgweb)
5. compile (detail / hgweb)
6. updated dependencies + compile (detail / hgweb)
7. moved 'realizers' into their own theory, now that they are decupled from the old datatype construction (detail / hgweb)
8. removed 'old_datatype' command (detail / hgweb)
9. don't test 'old_datatype', which is on its way out (detail / hgweb)
10. ported inductive realizer to new datatype package (detail / hgweb)
11. removed needless theorems (detail / hgweb)

Started by an SCM change (2 times)

This run spent:

• 1 hr 12 min waiting;
• 4 hr 58 min build duration;
• 6 hr 11 min total from scheduled to completion.