1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
\DOC ASSUME
\TYPE {ASSUME : term -> thm}
\SYNOPSIS
Introduces an assumption.
\KEYWORDS
rule, assumption.
\DESCRIBE
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}.
\EXAMPLE
{
# ASSUME `p /\ q`;;
val it : thm = p /\ q |- p /\ q
}
\COMMENTS
This is one of HOL Light's 10 primitive inference rules.
\SEEALSO
ADD_ASSUM, REFL.
\ENDDOC
|
