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.