Quoting :doc note-6-4:

  The :[loop-stopper] field of a rule of class :[rewrite], should still
  be a list of lists (var1 var2 fn1 fn2 ... fnk), where var1 and var2
  are variables and the fni are symbols. But formerly each fni was
  required to be a function symbol; now, it can be a macro alias for
  a function symbol (see [add-macro-alias]). For example, the
  following is a valid :[loop-stopper] field: ((x y +)).


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