The Control Component of Open Mechanized Reasoning Systems: Annotation and Tactics