delete useless sortingTheory.sorted_perm_eq

it is a trivial consequence of sortingTheory.SORTED_PERM_EQ
Tweak to x86-64 instruction encoder.
Update COPYRIGHT notice's years to include 2014.

I dislike claiming ownership like this; perhaps we should just put the
source code into the public domain outright.
Remove old documentation for tactics that don't exist anymore.
duplicate words removed from .doc files
consistent use of upper-case letters within enumeration
typo: sch(e)matic
consistens use of 'schema' (and not 'scheme') within a single .doc file
typo: a(n) HOL
more duplicate words removed from .doc files
missing dot added
typo: use '\ie' LaTeX macro instead of 'ie'
make non-script files in src/ non-executable
'make clean' should also remove auto-generated 'theorems.tex'

Otherwise 'git status' displays it as 'untracked'.
duplicate words removed from various documentation files

The magic command is:

grep " \([[:alpha:]]\+\) \1[[:space:]]" \
  `find . -name "*.doc" -or -name "*.tex"`

but the output still needs to be filtered by eye, since many duplicates
occur in embedded math and ML.

Duplicates in the Italian manual approved by Domenico Masini.
consistent use of "well-founded(ness)" instead of "wellfounded(ness)"

It was quite unfortunate to mix both forms (i.e. with and without
hyphen) within a single WF_REL_TAC.doc page.
minor fixes to hidden chapter of the manual
underscore in BibTeX keys means trouble: do not use it
no separate BibTeX database for Italian translation of the manual
BibTeX database cleanup

The cleanup follows the advices of two tools: bibcheck and bibclean.