Remove Globals.priming.

Also remove references to it in code that isn't being tested in the
regression checking build-sequence, and so is probably bit-rotted.

Provide numvariant version of variant, which behaves like

with_flag(Globals.priming,SOME "") (variant avoids)

Document change/incompatibility in release notes.

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

Split off the command syntax into a separate script, and made
a half-hearted attempt at defining a relational semantics using
measure theory from my thesis.

Ported the verification condition generator to the latest version of HOL, and tidied up its theory a bit (removed a couple of unnecessary constants). All the examples now work again.

Name changes in preparation for the addition of angelic choice

Aaron Coble's port to the latest version of HOL

Factorized out some common subexpressions as new definitions.

Some reorganization and name changes while I'm correcting my pGCL paper.

Started the process of getting the pGCL example back to a working state.

Updated TODO list, and incorporated a fix for a bug spotted by
Orieta Celiku.

A HOL example formalizing pGCL (Probabilistic Guarded Command Language).

pGCL supports both demonic and probabilistic choice, so can in principle
be applied to the verification of distributed random algorithms.

The high-point of this example is the verification of the probabilistic
voting scheme in Rabin's mutual exclusion algorithm.