command 'defaultsort' is renamed to 'default_sort', it works within a local theory context;

removed material that is out of scope of this manual;

renamed command 'defaultsort' to 'default_sort';

localized default sort;

more systematic naming of tsig operations;

modernized/simplified Sign.set_defsort;

get_sort: minimize sorts given in the text, while keeping those from the context unchanged (the latter are preferred); tuned;

export Type.minimize_sort;

term_typ: print styled term

merged

merged

generalize types of path operations

generalize more continuity lemmas

generalized many lemmas about continuity

simplify definition of continuous_on; generalize some lemmas

move intervals section heading

remove unused, redundant constant inv_on

reorganize subsection headings

remove redundant lemma

more lemmas to Vec1.thy

simplify proof

move more lemmas into Vec1.thy

move proof of Fashoda meet theorem into separate file

move definitions and theorems for type real^1 to separate theory file

removed obsolete sanity check -- Sign.certify_sort is stable;

monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;

really minimize sorts after certification -- looks like this is intended here;

tuned signature;

merged

tuned whitespace