Added a new proved lemma, state-p1-update-print-base, to axioms.lisp
so that "make proofs" doesn't break on guard verification for the
function set-print-base-radix.

Quoting :doc note-6-5:

  The function [pairlis$] is now tail-recursive, hence potentially more
  efficient. More precisely, its definition for the logic remains
  unchanged, but using [mbe], for execution it calls a new
  tail-recursive function, pairlis$-tailrec. Thanks to Jared Davis
  for requesting this improvement.


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1294 5d84a466-a78b-0930-a311-59b22171a541