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;

avoid catch-all exception handling;

eliminated fragile catch-all pattern, based on educated guess about the intended exception;

Attribute map_function -> coercion_map; tuned;

syntax category "real" subsumes plain "int";

merged