clarified tooltips: message output by default, extra info via control/command;

warn in correlation with report -- avoid spurious message duplicates;

tuned;

feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);

merged

updated SMT certificates

standardize timeout value based on reals

merged

merged

change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'

merged

renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun

renamed lemma cont2cont_Rep_CFun to cont2cont_APP

simplify proof of typedef_cont_Abs

rename constant trifte to tr_case

add 'LAM (Def x). t' as alternative syntax for 'FLIFT x. t'

make syntax of continuous if-then-else consistent with HOL if-then-else

rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff

polyml_as_definition does not require explicit dependencies on external ML files

explicit warning about opaque signature matching -- saves extra paragraph in implementation manual;

discontinued obsolete function sys_error and exception SYS_ERROR;

replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;

replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;

try_param_tac: plain user error appears more appropriate;

replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;

eliminated dead code;

more conventional exceptions for abstract syntax operations -- eliminated ancient SYS_ERROR; proper signature constraint;

removed assumption

more on naming tactics;

merged