merged

efficient construction of red black trees from sorted associative lists

more explicit code equations

adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc

special code setup for step function in IMP is redundant as definition was tuned (cf. c54d901d2946)

test case for set_comprehension_pointfree simproc succeeds now

unfolding bounded existential quantifiers as first step in the set_comprehension_pointfree simproc

moving simproc from Finite_Set to more appropriate Product_Type theory

generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)

adding some example that motivates some of the current changes in the set_comprehension_pointfree simproc

set_comprehension_pointfree also handles terms where the equation is not at the first position, which is a necessary generalisation to eventually handle bounded existentials; tuned

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;

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