ASSUME : term -> thm
STRUCTURE
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
HOL  Kananaskis-10