qed-

Saves the current interactive theorem or definition without indexing. Therefore automation will ignore it. In order to do this, the set of sequents still to be proved must be empty.