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
.