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.