CERTIFY-BOOK!

a variant of certify-book
Major Section:  OTHER

Examples:
(certify-book! "my-arith" 3)     ;Certify in a world with 3
                                   ; commands, starting in a world
                                   ; with at least 3 commands.
(certify-book! "my-arith")       ;Certify in the initial world.
(certify-book! "my-arith" 0 nil) ;As above, but do not compile.

General Form: (certify-book! book-name k compile-flg)

where book-name is a book name (see book-name), k is a nonnegative integer used to indicate the ``certification world,'' and compile-flg indicates whether you wish to compile the (functions in the) book.

This command is identical to certify-book, except that the second argument k may not be t in certify-book! and if k exceeds the current command number, then an appropriate ubt! will be executed first. See certify-book and see ubt!.