Library Nijn.Prelude.Checks
We use this command to guarantee that all subgoals are focussed.
Export
Set
Default
Goal
Selector
"!".