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

Replace a number of delsimps calls with temp_delsimps instead

The problem with delsimps is that it makes the change permanent for
all descendent theories.

Some proofs need adjusting as a result.

Be more careful over handling of ThmSetData and rebinding of thm names

In particular, it was previously possible to do

val thm = store_thm("thm[some_attribute]", tm1, tac2);
val thm = store_thm("thm", tm2, tac2);

and have the second thm be exported but to pick up the attribute from
the first call. This is clearly outrageous, so now the attribute is
lost when the second theorem is slotted into the theory.

Working through all this found three places where this
double-definition pattern was happening (there may yet be more). In
src/finite_map and src/list the second theorem was clearly just
redundant and could be deleted.

The example in fun-op-sem is slightly more interesting: there it
defines a function (which definition gives that function a "compute"
attribute), and then restates the definition, saving it under the same
name ("foo_def"). Though arguably bad style, it's important that the
second theorem replace the first, and that it should have the
"compute" attribute. Here the change is to explicitly add that
attribute to the second theorem.

Finally, all this work revealed that Theory.sml's handling of the
NewBinding theory-delta hook was wrong and caused changes to be
dropped after the hook function was called. Debugging *that* led me to
add a pp field to the LoadableThyData registration process so that
theory-data values could be inspected more easily. There is also a
trace variable to turn on some debugging output in Theory.

Get fun-op-sem/for to build again

Add it to the build sequence

Fix Q.GENL to handle variables in same order as GENL.

Closes #428

Fix fun-op-sem example

It was broken by changes in abbreviated simplification tactics.

added a comparison with Charguéraud' Pretty Big Step approach

Yong Kiam and I did most of the development for this commit.

update fun-op-sem example

fun-op-sem: improved file structure, more comments