EXPAND_TAC : string -> tactic

SYNOPSIS
Expand an abbreviation in the hypotheses.

DESCRIPTION
The tactic EXPAND_TAC "x", applied to a goal, looks for a hypothesis of the form `t = x` where x is a variable with the given name. It then replaces x by t throughout the conclusion of the goal.

FAILURE CONDITIONS
Fails if there is no suitable assumption in the goal.

EXAMPLE
Consider the final goal in the example given for ABBREV_TAC:
  val it : goalstack = 1 subgoal (1 total)

   0 [`12345 + 12345 = n`]

  `n + f n = f n`
If we expand it, we get:
  # e(EXPAND_TAC "n");;
  val it : goalstack = 1 subgoal (1 total)

   0 [`12345 + 12345 = n`]

  `(12345 + 12345) + f (12345 + 12345) = f (12345 + 12345)`

SEE ALSO
ABBREV_TAC.