remove unnecessary simp rules involving Abs_Integ

introduced option "z3_with_extensions" to control whether Z3's support for nonlinear arithmetic and datatypes should be enabled (including potential proof reconstruction failures)

merged

remove pretty syntax for FinFuns at the end and provide separate syntax theory

add lemma set_of_image_mset

merged

eliminated remaining sub- and superscripts in FinFun syntax

syntax for FinFun composition without subscripts tuned proofs

FinFun pseudo-constructor syntax without superscripts

replace FinFun application syntax with $

removed subscripts from FinFun type syntax

improve code setup for set equality

add code equation for coset xs = set ys

tuned proofs

use bundle in FinFun

unify Rep_finfun and finfun_apply

move FinFuns from AFP to repository

discontinued unused unzip/untar;

update GUI components after init;

merged

don't be so aggressive during unfolding id and o

reordered sections

tuned message;

separate syslog dockable -- discontinued tendency of sub-window management via tabs;

clarified prover startup: no timeout, read stderr more carefully;

need to close_input before expecting threads to terminate/join; tuned signature;

make double sure that GUI components are up-to-date after init;

tuned message;

more explicit treatment of return code vs. session phase;

tuned signature;