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

DISCH : term -> thm -> thm

SYNOPSIS

Discharges an assumption.

DESCRIPTION

       A |- t
--------------------  DISCH `u`
 A - {u} |- u ==> t

FAILURE CONDITIONS

DISCH will fail if `u` is not boolean.

COMMENTS

The term `u` need not be a hypothesis. Discharging `u` will remove any identical and alpha-equivalent hypotheses.

EXAMPLE

  # DISCH `p /\ q` (CONJUNCT1(ASSUME `p /\ q`));;
  val it : thm = |- p /\ q ==> p