consolidated names of theorems on composition; generalized former theorem UN_o; comp_assoc orients to the right, as is more common

corrected NEWS

avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient; more elementary level_list: avoid stack overflow; prefer elementary graph operations; tuned;

clarified long_names -- conform to usual Isabelle practice of not analysing internal names;

more precise repaint and revalidate -- the latter is important to keep in sync with content update;

tuned;

prefer synchronous Mutator_Event.Bus on Swing_Thread;

more direct tooltip content;

tuned;

use Pretty_Tooltip for Graphview_Panel; tuned signature;

more basic tooltips;

close tooltips more thoroughly;

make buttons closer to original mouse position;

detach tooltip as dockable window;

explicit close button;

congruence rule for Finite_Set.fold

alternative simplification of ^^ to the righthand side; lifting of comp_fun_commute to ^^

eliminated obsolete tooltip delay -- bypassed by Pretty_Tooltip;

merged

newer versions of Z3 call it "Bool" not "bool"

simplified type of msetprod; n.b. image function need not be part of minimal definition of msetprod, since multisets may already contain repeated elements

tuned proof

default simp rule for image under identity

dropped duplicate facts; tuned syntax

more facts on setsum and setprod

made SML/NJ happier

do not expose details of internal data structures for composition of BNFs

further support for nested tooltips;

tuned proofs;

refer to parent frame -- relevant for floating dockables in particular;

tuned window position to fit on screen;

tuned window position;

determine window size from content;

tuned color and font size;

close tooltip window on escape; tuned;

proper message markup for output;

some re-ordering of initialization to ensure proper formatting;

separate module Pretty_Tooltip;

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