hint

Displays a list of theorems that can be successfully applied to the current selected sequent. The command is removed from the script, but the window that displays the theorems allow to add to the script the application of the selected theorem.