added lemmas contributed by Rene Thiemann

attach modifier only later, to avoid interference as e.g. in "simp add: foo [simplified] bar";

tuned whitespace;

clarified ML toplevel pp: avoid ML output to be attached to inlined binding positions;

merged

made SML/NJ happy;

clarified Method.section: explicit declaration with static closure;

tuned signature -- define some elementary operations earlier;

discontinued odd "temporary" workaround from 2006 (6ac7a4fc32a0), which has no measurable relevance;

tuned;