removed obsolete markup for "open_block" (see also d5ad89fda714): Isabelle/Scala directly supports XML.Elem pretty-printing;

Library material from Eberl's Parallel_Shear_Sort

Trying to clean up these horribly ugly old proofs, but the requirement of constructivity makes it very difficult

use automatically generated time function in HOL-Data_Structures.Selection

merged

better time_functions (let)

less hidden configuration;

proper passwordless smtp check: must be null;

adjusted documentation

more attribute tuning

tuned attributes

merged

added lemmas

tuned proofs;

tuned NEWS;

markup for "..." notation; clarified signature;

more robust: avoid non-authentic translations;

tuned whitespace of sources;

update documentation; tuned typesetting;

tuned;

update documentation: print mode "latex" only affects syntax tables, but output of symbols;

misc tuning and clarification;

clarified section structure;

tuned;