A variant of certify-book
(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! 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)
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!.