Updated comments for compression functions

Removed unfold:thm from signature INTR_ELIM and from the functor result. It is never used outside, is easily recovered using bnd_mono and def_lfp_Tarski, and takes up considerable store.

Now mutual_induct is simply "True" unless it is going to be significantly different from induct -- either because there is mutual recursion or because it involves tuples.

fixed indentation

New version of type sections and many small changes.

Note that unfold is not exported, that mutual_induct can be omitted (as the trivial theorem True), and comments on storage Also uses Datatype instead of Univ/Quniv as parent theory for lists, and omits quotes around types in theory files.

Added line breaks and other cosmetic changes