Provide tactic to update an abbreviation

[mn200]

  update_abbrev : thm -> tactic

takes a theorem of the form v = t (and maybe also t = v), finds an Abbrev of the form Abbrev(v = t0) in the assumptions, and replaces the t0 with t.