Latex allows to set pointsize at 10pt, 11pt or 12 pt, but this does not work
with Knuth's macro \bigg#1. There seem to be two problems, one easily
fixed, and the other seeminly hard. The easy fix: change 14.5pt in
\vbox\to\14.5pt{} to 1.45em. The hard part is that the parameter #1
comes out in 10pt size, regardless of the point size chosen on the
\documentstyle line of the .tex file. The same problem exists of course
with all macros related to \bigg.