remove executable bit from text files in examples/

Move the pretty-printing facilities around a bit so that both SML
implementations use our own version of the PP structure. This
implementation is called HOLPP in src/portableML. After the kernel's
Overlay.sml is loaded, it is also available under the name PP. This
retains fairly good backwards incompatibility. The one deliberate
incompatibility is to make references to General.ppstream invalid.
This makes us better conform with Basis 2002.

The advantage of this manoeuvre is to allow me to better control what
our pretty-printers do at a low level.

added theories for dining cryptos example, information theory, probability theory, measure theory, and lebesgue integration