added lemma

Removed multiplicativity assumption from normalization_semidom

clarified file names;

clarified build_polyml_component: include IDE entry point for ML compiler;

merged

tuned spelling;

new examples of BNF lifting across quotients using a new theory of confluence, which simplifies the relator subdistributivity proof obligation (a few new useful notions were added to HOL; notably the symmetric and equivalence closures of a relation)

Removed unnecessary and problematic trivial lemma from HOL-Algebra

proper executable file;

more documentation: odd option for special situations;