reintroduced "metis" call taken out after reintroducing "set" as a constructor, and added two "metis" calls that used to be too slow

update docs to reflect "Manual_Nits"

removed special handling for set constants in relevance filter

reintroduced Sledgehammer call taken out by 9bc924006136, with some hints to guide the naive relevance filter

killed unfold_set_const option that makes no sense now that set is a type constructor again

tuned

removed unnecessary lemmas

tuned proofs

tuned var names

tuned argument order

merged

add simp rules for bitwise word operations with 1

tuned types

disabled failing sledgehammer unit test (collateral damage of 184d36538e51)

disabled kodkodi in mira runs as well (cf. 493d9c4d7ed5)

merged

Made gen_dest_case more robust against eta contraction

merged

remove unnecessary intermediate lemmas

tuned;

eliminated old-fashioned Global_Theory.add_thms;

simplified proof -- avoid res_inst_tac, afford plain asm_full_simp_tac;

simplified proof;

simplified proof;

simplified proof;

more parallelism;

tuned;

merged

tuned -- afford slightly larger simpset in simp_defs_tac;

tuned -- standard proofs by default;