refined rich tooltip options; basic tooltips without markup;

Rich_Text_Area tooltips via nested Pretty_Text_Area, based on some techniques of FoldViewer plugin;

some documentation of show_markup;

tuned proofs;

option to bypass potentially slow text overview;

tuned signature;

clarified platform dependency;

updated crontab and afp-poly settings

thread the right local theory through + reenable parallel proofs for previously problematic theories

made code more conform to rest of BNF package

more error positions;

more explicit show_type_constraint, show_sort_constraint;

recovered print translation after 'a => bool to 'a set change;

tuned;

use explicit Type.strip_sorts_dummy to suppress sort constraints in output;

printed "_ofsort" is subject to show_markup as well;

allow position constraints to coexist with 0 or 1 sort constraints; more position information in sorting error; report sorting of all type variables;

made tactic more robust (less usage of stac)

continued changing type of corec type

removed dead params and dead code

changed type of corecursor for the nested recursion case

made (co)rec tactic more robust when the simplifier succeeds early

tuned;

removed unused module Blob;

more direct message header: eliminated historic encoding via single letter;

tuned whitespace;

tuned proofs;

report sort assignment of visible type variables;