CLAIM_TAC : string -> term -> tactic
# g `(p <=> q) ==> p \/ ~q`;; val it : goalstack = 1 subgoal (1 total) `(p <=> q) ==> p \/ ~q` # e DISCH_TAC;; val it : goalstack = 1 subgoal (1 total) 0 [`p <=> q`] `p \/ ~q`
# e(CLAIM_TAC "yes|no" `p /\ q \/ ~p /\ ~q`);; val it : goalstack = 3 subgoals (3 total) 0 [`p <=> q`] 1 [`~p /\ ~q`] (no) `p \/ ~q` 0 [`p <=> q`] 1 [`p /\ q`] (yes) `p \/ ~q` 0 [`p <=> q`] `p /\ q \/ ~p /\ ~q`