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