some support for editor perspective;

discontinued redundant Edit_Command_ID;

reduced warnings;

tuned message;

old-style numbered structure index is legacy feature (hardly ever used now);

added official Text.Range.Ordering; some support for text perspective;

tuned signature;

reverted some odd changes to HOL/Import (cf. 74c08021ab2e);

merged

modernized specifications

removed session HOL/Subst -- now subsumed my more modern HOL/ex/Unification.thy

removed technical or trivial unused facts

more precise authors and comments; tuned order and headers

added proof of idempotence, roughly after HOL/Subst/Unify.thy

tuned proofs, sledgehammering overly verbose parts

tuned notation

ported some lemmas from HOL/Subst/*; tuned order

changed constant names and notation to match HOL/Subst/*.thy, from which this theory is a clone.

merged

add lemmas interior_Times and closure_Times

avoid pred/set mixture

avoid pred/set mixture

merged

remove unnecessary euclidean_space class constraints

section -> subsection

scale dependency graph to fit on page

more robust initialization of token marker and line context wrt. session startup;

tuned Parse.group: delayed failure message;

avoid actual Color.white, which would be turned into Color.black by org.gjt.sp.jedit.print.BufferPrintable;

default style for user fonts -- to prevent org.gjt.sp.jedit.print.BufferPrintable from choking on null;

tuned;

discontinued somewhat pointless Par_List.map_name -- most of the time is spent in tokenization;