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

merged

tuned proof

tuned proof

tuned lemma proposition of properties_for_sort_key

lemmas sorted_map_same, sorted_same

lemmas multiset_of_filter, sort_key_by_quicksort

more on "Time" in Isabelle/ML;

simplified some time constants;

added convenience operation seconds: real -> time;