ASSUME : term -> thm

SYNOPSIS

Introduces an assumption.

DESCRIPTION

When applied to a term t, which must have type bool, the inference rule ASSUME returns the theorem t |- t.

   --------  ASSUME `t`
    t |- t

FAILURE CONDITIONS

Fails unless the term t has type bool.

EXAMPLE

  # ASSUME `p /\ q`;;
  val it : thm = p /\ q |- p /\ q

COMMENTS

This is one of HOL Light's 10 primitive inference rules.

SEE ALSO

ADD_ASSUM, REFL.