qed

Saves and indexes the current interactive theorem or definition. In order to do this, the set of sequents still to be proved must be empty.