Make output from Count.report more compact, which in turn affects Count.apply.

At the same time clean-up the code.

If folks prefer the more wordy reporting then a flag could be introduced for switching between the two styles.

Thm.ETA_CONV -> Drule.ETA_CONV, Thm.Eta -> Drule.RIGHT_ETA

Cursory profiling indicates that an implementation of ETA_CONV as a primitive
inference rule in Thm is about 20 times faster than an implementation as a
derived rule that instantiates ETA_AX, but that the difference in overall HOL
build time is negligible.

Please do let me know if you encounter (performance) problems due to this
change.

Provide better documentation for theorem-counting facilities. In passing,
adjust behaviours so that Count.apply and Lib.time make reports even
if the functions they are measuring raise exceptions.

Pretty significant "refactoring" of the early source code. All the stuff
that was in common between 0 and experimental-kernel moves into a new
prekernel directory. This can be thought of as the kernel utilities
directory, full of code that is not quite portableML because it's fairly
HOL specific, but that isn't really part of the core implementation of
types, terms and theorems.
(Also add a new pair_compare function to Lib.)