INTRO_TAC : string -> tactic
# g `!p q r. p \/ (q /\ r) ==> p /\ q \/ p /\ r`;; # e (INTRO_TAC "!p q r; p | q r");; val it : goalstack = 2 subgoals (2 total) 0 [`q`] (q) 1 [`r`] (r) `p /\ q \/ p /\ r` 0 [`p`] (p) `p /\ q \/ p /\ r`
# e (INTRO_TAC "#1");; val it : goalstack = 1 subgoal (2 total) 0 [`p`] (p) `p /\ q`