ASSUME : term -> thm
STRUCTURE
Thm
SYNOPSIS
Introduces an assumption.
LIBRARY
HolKernel
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
Fails unless the term t has type bool.
SEEALSO
ADD_ASSUM, REFL
HOL  Kananaskis-13