.big {
	font-size: 250%;
}

.dim-highlight {
	color: gray;
}

.machine {
	padding-left: 0;
	padding-right: 0;
}

.pd-bottom {
	padding-bottom: 0.5em;
}

.ctrl-heading {
	color: gray;
}