Tag Mario's name as UOK in comments at head of wlogLib.{sig,sml}

Tidy up copyright documentation

- Move some information out of file headers into various files in
doc/copyrights.
- Reinstate a LICENSE file for examples/muddy (which is LGPL).
- Identify code taken directly from Poly/ML implementation in
tools-poly/holrepl.ML

See github discussion at

https://github.com/HOL-Theorem-Prover/HOL/issues/559

for more on this.

Closes #559

Move without loss of generality tacticals to new library.