improved interleaving of start_execution vs. cancel_execution of the next update;

tuned proofs;

always revisit nodes independently of "required" flag, which may change during editing -- avoid "bloodbath effect" when changing perspective while loading;

tuned;

simplified internal actor protocol;

builtin timing for main operations;

add secondary transfer rule for universal quantifiers on non-bi-total relations

move definition of set_rel into Library/Quotient_Set.thy

add transfer rule for 'id'

add new transfer rules and setup for lifting package

setup_lifting preprocesses forall_transfer rule by unfolding mem_Collect_eq

NEWS

hide code generation facts in the Float theory, they are only exported for Approximation

merged

forgot to add file

make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules

merged

NEWS

transfer now handles Let

merged

added revised version of Abs_Int

add transfer rule for Let

add code lemmas for word operations

tuned whitespace

dropped dead code

rename no_code to no_abs_code - more appropriate name

use tnames for bound variables in rsp thms

true delayed evaluation of "SPASS_VERSION" environment variable

merged

use latest Z3

merged

reorganised IMP