Move stuff into HOL/examples (upgrade!); progress w/completeness.

The necessary HOL commit is 33ec65435c.