STD updates
  - Prevent "wrong" b* binder usage for defaggregates (see issue 41)
  - Tweak extended formals parsing with additional error checking (fixes issue 57).

Various, minor cleanups
  - Remove stubs from acl2 6.4
  - Tweak .gitignores
  - Minor updates to copyright headers

Update issue 41

Issue 41 is right -- the current behavior is unintuitive and bad.  But it's
scary to change the defaggregate b* binders to automatically bind the variable
(which we didn't previously do) since we might then inadvertently change the
behavior of existing code that relies on the old behavior.

As a way forward, this patch adds code to detects and cause errors in scary
cases like

    (b* (((my-aggregate x) (f ...)))
       <body>)

where <body> mentions X.  It's smart enough to allow cases like

    (b* (((my-aggregate x) x))
       <body>)

Since here there's no confusion.  We can leave this error detection in for
awhile (say through the 6.5 release) to make sure that no existing code has
these problems.  Then (say right after the 6.5 release) we can remove this
restriction and simply have the b* binder always bind X, as well.

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2418 303c5b2c-9740-0410-b014-fd8f9db7be32