Disabledp accepts runic abbreviations such as (:d append).  Added bin/ scripts to help ensure "purity" of ACL2 sources.

Quoting :doc note-7-0:

  The utility [disabledp] now accepts runic abbreviations such as (:d
  append). (See [theories] for a discussion of runic abbreviations.)
  Thanks to Shilpi Goel for requesting this enhancement.

Added preliminary scripts bin/purity.sh and bin/pull.sh to help ensure
"purity", i.e., that only ACL2 authors write to other than books/.
Thanks to many people for helping me with git (David, Jared, Keshav,
Shilpi, Sol).

Added/updated some .gitignore files.