Quoting :doc note-6-5:

  When forcing (see [force]) is applied, we now always see the
  appropriate [executable-counterpart] [rune],
  (:executable-counterpart force), in the proof output and summary;
  this hadn't previously been the case. Thanks to Robert Krug for
  bringing this issue to our attention.


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