Quoting :doc note-7-0:

  When the [ld-evisc-tuple] is non-nil, the utilities :[pe], :[pc], and
  :[pbt!] now abbreviate their output accordingly. See
  [set-evisc-tuple]. Thanks to David Rager for bringing the need for
  this change to our attention.

Removed AND-LIST and OR-LIST from *primitive-logic-fns-with-raw-code*.


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1384 5d84a466-a78b-0930-a311-59b22171a541
Added comments in legal-variable-or-constant-namep about possibly
changing symbols with name "*" from being considered constants to
being considered variables (and issue raised recently by Harsh and
Pete).

Quoting :doc note-7-0:

  The heuristics have changed for guessing the :typed-term field for a
  :[type-prescription] rule when that field is not explicitly
  specified. Specifically, consider the case that the conclusion of
  the rule is a function call (p u) for some term u, such that there
  is an enabled [compound-recognizer] rule for p. Formerly, the
  :typed-term was u in this case. Now, it must be the case that the
  most recent enabled such [compound-recognizer] rule is `strong', in
  the following sense: if ts1 is the [type-set] implied by assuming
  the conclusion true and if ts2 is the [type-set] implied by
  assuming the conclusion false, then ts1 and ts2 are complementary.
  Thanks to Jared Davis for an email that prompted us to make this
  change.


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