Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
UNDISCH_TAC : term -> tactic

SYNOPSIS
Undischarges an assumption.

DESCRIPTION
          A ?- t
   ====================  UNDISCH_TAC `v`
    A - {v} ?- v ==> t

FAILURE CONDITIONS
UNDISCH_TAC will fail if `v` is not an assumption.

COMMENTS
UNDISCHarging `v` will remove all assumptions that are alpha-equivalent to `v`.

SEE ALSO
DISCH, DISCH_ALL, DISCH_TAC, DISCH_THEN, STRIP_TAC, UNDISCH, UNDISCH_ALL, UNDISCH_THEN.