Updating: tidying up a bit
Updating: minorly improving DiningPhil
Updating: minorly improving documentation.
Replaced dollar sign with underscore in symbol names.