===== rotate_tac ===== Rotates the assumptions by k positions to the left. It can be used to influence which assumption is unified when using methods like ''[[drule]]'', ''[[frule]]'', ''[[erule]]'' or even ''[[assumption]]''.