Certify-book!
A variant of certify-book
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.
General Form:
(certify-book! book-name k compile-flg)
where book-name is a book filename, 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!.
