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