Quoting :doc note-6-4, and following a suggestion from J:

  The wording in theory warnings has been improved, to avoid giving the
  impression that you are newly disabling a built-in rule in the case
  that it merely remains disabled.

To elaborate: formerly, if a rule had been disable and then an
in-theory event left it disabled, you might see this warning:

  ACL2 Warning [Theory] in ( IN-THEORY (DISABLE ...)):  Although the
  theory expression (DISABLE MV-NTH) disables the :DEFINITION rule for
  MV-NTH, some expansions involving this function may still occur.  See
  :DOC theories-and-primitives.

Now you'd see this warning, which avoids giving the impression that
you are newly disabling the rule.

  ACL2 Warning [Theory] in ( IN-THEORY (CURRENT-THEORY ...)):  The :DEFINITION
  rule for MV-NTH is left disabled by the theory expression 
  (CURRENT-THEORY :HERE), but because this function is built-in in some
  way, some expansions of its calls may still occur.  See :DOC theories-
  and-primitives.

Made minor GNUmakefile fixes for doc.lisp target.


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

Made minor Makefile improvements, and updated doc.lisp.


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