Removed some obsolete GCL-specific directives; minor :doc fixes.

Thanks to David Rager for emails leading to the :doc fixes.

For GCL, now we now require version GCL 2.6.12 or later, I removed the
following from a few .acl2 files, which was probably important for GCL
2.6.8 for avoiding space exhaustion, but not for GCL 2.6.12.

(setq si::*optimize-maximum-pages* nil)

Thanks to Camm Maguire for pointing this out.  I saw some significant
speed-ups with this change, for example, in ACL2(h), for
books/misc/misc2/reverse-by-separation.cert.out, the realtime was
reduced from 251.66 seconds to 205.63 seconds.

These are the changed files, with notes about some:

books/centaur/vl/kit/cert.acl2
  left a comment since this wasn't tested (perhaps requires quicklisp)

books/centaur/vl/cert.acl2.orig
  also removed (setq si::*multiply-stacks* 2)

books/centaur/vl/top.acl2.orig

books/misc/misc2/reverse-by-separation.acl2.orig

books/workshops/2009/sumners/support/kas.acl2.orig
  also removed (setq si::*multiply-stacks* 2)