Minor edit for proofs.

remove lcsymtacs (github issue #666)

The lcsymtacs structure is regarded superseded as it plainly is
a shorthand for opening the following modules:
Abbrev HolKernel boolLib Tactic Tactical BasicProvers simpLib
Rewrite bossLib Thm_cont

Fix various breakages caused by 86935be3f42

Along the way adjust WORD_CANCEL_CONV to tidy up after itself so
that when it sees

x + y + z + u = a + y + b + u

it doesn't turn it into

x + y + z + u - y - u = a + y + b + u - y - u

and wait for something else to clean it up, but rather goes straight
to

x + z = a + b

Update scripts for the revised AKS paper.

AKS mechanisation (#750)

* Add to examples: AKS, with algebra and simple_complexity.