BIG.tty 


(NEWFONT size)
The function NEWFONT sets up default fonts to be "size", where size is one of the atoms BIG, MEDIUM, STANDARD, SMALL. Changes the prettyprint fonts, the default font for the break window, typin, etc. Does this by resetting FONTPROFILE and then setting the fonts for all of the known windows.