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!.
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!.