ONCE_REWRITE_TAC : thm list -> tactic
# let thl = map (num_CONV o mk_small_numeral) (1--3);; val thl : thm list = [|- 1 = SUC 0; |- 2 = SUC 1; |- 3 = SUC 2]
# g `0 < 3`;; val it : goalstack = 1 subgoal (1 total) `0 < 3`
# e(ONCE_REWRITE_TAC thl);; val it : goalstack = 1 subgoal (1 total) `0 < SUC 2`
# e(REWRITE_TAC thl);; val it : goalstack = 1 subgoal (1 total) `0 < SUC (SUC (SUC 0))`