The Control Layer in Open Mechanized Reasoning Systems: Annotations and Tactics