respect font property for symbols

capitalize lowercase groups; tuned with mkString

merged

more generous timeout for SML/NJ, which is approx. 40-80 times slower than Poly/ML; more generous timeout for HOL-Quickcheck_Examples, which is rather slow in checking its examples (and mostly sequential);