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

Rename DROP_NIL to DROP_EQ_NIL

No longer ugly collision with DROP_nil and more consistent naming with how
other thms from the same theory are named.

Also replace >= with <=.

Remove trailing whitespace throughout examples/

update fun-op-sem example