Tej Chajed authored Sep 15, 2020 and Robbert Krebbers committed Sep 15, 2020

Set Default Goal Selector "!" makes it illegal to ever apply a tactic
with more than one goal (instead, must focus with bullets or braces).