more consistent error messages on malformed code equations

removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands; removed '(open)', '(set_name)' and '(open set_name)' options

use Set.filter instead of Finite_Set.filter, which is removed then

rename Set.project to Set.filter - more appropriate name

added some ad-hoc namespace prefixes to avoid duplicate facts;

avoid duplicate facts;

more explicit namespace prefix for 'statespace' -- duplicate facts;

eliminated spurious fact duplicates;

modernized dynamic "rules" -- avoid rebinding of static facts;

removed redundant lemma, cf. class zero_neq_one in HOL/Rings.thy;

clarified Element.init vs. Element.activate: refrain from hard-wiring Thm.def_binding_optional to avoid duplicate facts;

tuned;

clarified Local_Defs.add_def(s): refrain from hard-wiring Thm.def_binding_optional; clarified Generic_Target.define: avoid duplicate def binding via Local_Defs.add_def;

more explicit flags for facts table;

minor tuning;

more conventional Double constants;

tuned source structure;

tuned;

tuned;

merged

added type annotations to generated Isar proofs -- code by Steffen Smolka

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;