Alter VAR_EQ_TAC to call TIDY_ABBREVS after invocation

TIDY_ABBREVS "purges" abbreviations that have become malformed, where

- "malformed" means no longer of form Abbrev (var = exp), with exp not
itself a variable
- "purge" means Abbrev(e1 = e2) becomes e2 = e1, and Abbrev(other_exp)
becomes other_exp.

The action of TIDY_ABBREVS is included in the ABBREV_ss simpset
fragment, which is in turn included in the stateful simpset.

The calling of TIDY_ABBREVS is the only change in the behaviour of
VAR_EQ_TAC, and this can be turned off with the
BasicProvers.var_eq_old trace.

Fixes for changes to VAR_EQ_TAC etc.

Fix generic_finite_graphs to properly record incoming edges

This has some knock-on effects in the examples/logic/ltl directory.

added acceptance sets to gba type

Fixes to build logic/ltl/concrGBArepScript.sml on --expk

finished expgba correct

started working on FINAL and TRANS

finished INIT, started on FINAL

finished states for concrwaa2gba, started with init

finished expGBA_reachable

working on reachable states of concrete gba

working on concrete waa2gba function

working on correspondance between concrete and abstract acceptance sets

working on states for concrete waa2gba

working on termination of concr waa2gba

working on termination of concrwaa2gba

progress on termination of waa2gba

Some progress on showing that the concrete extr_trans functions
corresponds to the abstract one

addNode Lemma for GBA

Adapted d_conj_concr so all lists will be nubbed
Showed how gba_trans_concr relates to d_conj_set

added new concrGBA file and some helpers to generHelpers and concrltl2waa