1\DOC ADD_ASSUM
2
3\TYPE {ADD_ASSUM : term -> thm -> thm}
4
5\SYNOPSIS
6Adds an assumption to a theorem.
7
8\KEYWORDS
9rule, assumption.
10
11\DESCRIBE
12When applied to a boolean term {s} and a theorem {A |- t}, the
13inference rule {ADD_ASSUM} returns the theorem {A u {s} |- t}.
14{
15       A |- t
16   --------------  ADD_ASSUM s
17    A u {s} |- t
18}
19
20\FAILURE
21Fails unless the given term has type {bool}.
22
23\SEEALSO
24Thm.ASSUME, Drule.UNDISCH.
25\ENDDOC
26