body {margin:  20pt;
    padding: 10pt;
    font-family: Times New Roman, Times;
    font-size: 13pt;
}

.racketcode{
	font-family:"Courier New", Courier, monospace;
	font-size:14px;
	color:#039;
}

.varname{
    color: #aa1189;
    font-family: Courier;
}

.note {
    font-style: italic;
    color: #002255;
}

.opt{
    background-color: #edddff;
    padding: 10px;
}