Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
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.