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.

Delete trailing whitespace in examples

rearranged fields of alternating automaton type

finished expgba correct

working on concrete waa2gba function

working on correspondance between concrete and abstract acceptance sets

working on states for concrete waa2gba

progress on termination of waa2gba

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

Strengthened the invariant of waa expansion, the followers list is
such that if the edge_grps coincide, then the entire labels
coincide

addNode Lemma for GBA

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

working on d_conj_set lemm for concrete gba

finished trans rel extraction proof

new helpers for invariants of expandAuto

showed some invariants for addfrml and addedge

removed unneeded stuff

finished addedge lemma

working on extracting concrete transition relation

still working on extracting transition relation

working on extracting trans

finished edge_grp counter lemm

working on concr waa transition relation

working on addEdgeLemm

working on trans for LTL to WAA

proved correctness for final states and atomic propositions

working on correctness of concrete initial states

Rewrote expand function so that it only operatos on the graph, not on the entire automata

working on concrete version of ltl to waa

working on correctness for concrete ltl -> waa

Working on correctness of concr ltl to waa translation
commented out most of the code on merge states for waa
and changed reachability relation to use RTC

Proved termination of concrete ltl -> waa using multiset ordering
Working on correctness of concrete ltl -> waa

still working on termination of concrete ltl -> waa

continued working on termination

working on termination for first translation

working on concrete version of ltl->waa

started working on concrete representation