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`
# g `!a. ~(a = 0) ==> ONE_ONE (\n. a * n)`;; # e (REWRITE_TAC[ONE_ONE; EQ_MULT_LCANCEL]);; val it : goalstack = 1 subgoal (1 total) `!a. ~(a = 0) ==> (!x1 x2. a = 0 \/ x1 = x2 ==> x1 = x2)` # e (INTRO_TAC "!a; anz; ![n] [n']; az | eq");; val it : goalstack = 2 subgoals (2 total) 0 [`~(a = 0)`] (anz) 1 [`n = n'`] (eq) `n = n'` 0 [`~(a = 0)`] (anz) 1 [`a = 0`] (az) `n = n'`