DISCH_ALL : thm -> thm
A1, ..., An |- t ---------------------------- DISCH_ALL |- A1 ==> ... ==> An ==> t
# end_itlist CONJ (map ASSUME [`p:bool`; `q:bool`; `r:bool`]);; val it : thm = p, q, r |- p /\ q /\ r # DISCH_ALL it;; val it : thm = |- r ==> q ==> p ==> p /\ q /\ r