Migrated all prob scripts to latest probabilityTheory with two cheats left

Reorganise files under examples/miller.

In particular, combine formalizeUseful, subTypeUseful and
ho_proverUseful into one HurdUseful that is in its own directory.
Also, put Know and Suff tactics into that library so that they don't
need to be repeatedly redefined at the head of the various Script
files.

Ported the Miller-Rabin example to the latest snapshot version of HOL4
(although it's only been tested with the experimental kernel). I'm
sure you don't wish to know, but I'm going to tell you anyway what
were the main offenders in making this port so painful:

* The addition of o_THM to std_ss, because o is used everywhere in my
formalization of probability theory to construct sets and functions
with specific properties.

* When set comprehensions are expanded the bound variables get
sensible names instead of variations on x. Thanks to whoever did
this, but it certainly required a lot of changes to existing proofs.

* My own terrible proof style at the time :-)

Prompted by Konrad's useful change to the AC stuff in the simplifier,
I have "fixed" a long-standing irritation in the associativity theorems
in pred_setTheory: they're the wrong way round. All other associativity
theorems in the system are oriented x _ (y _ z) = (x _ y) _ z, which is
the direction that AC_CONV expects. So, I've put them right. The changes
I had to make in pred_setScript are such that the proofs no longer depend
on any particular orientation, so this could always be changed back without
much grief.
Elsewhere, probability is the only place in the core distribution where
problems arose. There, and in the examples where similar things happened,
I replaced all occurrences of {UNION,INTER}_ASSOC with
GSYM {INTER,UNION}_ASSOC.
I also fixed the m scripts in the examples/miller so that they cause a
stop when they hit an error.
Finally, I changed developers/build-examples to clean up in the miller
directory before building. This is consistent with what is done for all
of the other examples.

Many changes due to the removal of ETA_CONV from the standard simpset.

This example is a verification of the Miller-Rabin probabilistic
primality test incorporating version 2 of probability theory and some
cute example probabilistic programs.

The reason I haven't incorporated it into src/ is that it takes about
2 hours to build, and carries a lot of `baggage' from my experiments
with proof tools.

The most convenient way to build it is change to the examples/miller/
directory, and use the `m' bash script (it also understands `m clean'
to clean the directories). If this doesn't work, or you can't do this,
then there's a longer version:

cd ho_prover
Holmake --qof
cd ../subtypes
Holmake -I ../ho_prover --qof
cd ../RSA
Holmake --qof
cd ../formalize
Holmake -I ../ho_prover -I ../subtypes -I ../RSA --qof
cd ../prob
Holmake -I ../ho_prover -I ../subtypes -I ../RSA -I ../formalize --qof
cd ../groups
Holmake -I ../ho_prover -I ../subtypes -I ../RSA -I ../formalize --qof
cd ../miller
Holmake -I ../ho_prover -I ../subtypes -I ../RSA -I ../formalize -I ../prob -I ../groups --qof
cd ..

It does build RIGHT NOW, but is quite sensitive to changes in the HOL
proof tools. I'll try and support it (especially if anyone uses it),
but sadly it might become more trouble than it's worth.