Updates to HOL/Algebra: - axclasses consolidated (lemma one_not_zero) - summation operator SUM removed, now uses setsum Use of setsum made it necessary to relax sort constraint in its definition to {zero, plus}.

tuned;

lower priority for forw_subst;

tuned;

not used any more (all Isar style)

removed MicroJava/Digest.thy

tuned for 99-2 release

unsymbolized; tuned;

tuned;

improved;