merged

"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}" by the new simproc defColl_regroup. More precisely, the simproc pulls an equation x=t (or t=x) out of a nest of conjunctions to the front where the simp rule singleton_conj_conv(2) converts to "if".

merged

continuity proofs for approx function on deflations; lemma cast_below_imp_below

allow lazy domain arguments to have class cpo

add cpo_type function

fix domain package parsing of lhs sort constraints

export quiet_mode and trace_domain refs for domain package

new lemma

merged