SEQ_IMP_REWRITE_TAC : thm list -> tactic
# g `!a b c. a < b ==> (a - b) / (a - b) * c = c`;; val it : goalstack = 1 subgoal (1 total) `!a b c. a < b ==> (a - b) / (a - b) * c = c` # e(IMP_REWRITE_TAC[REAL_DIV_REFL;REAL_MUL_LID;REAL_SUB_0; REAL_LT_IMP_NE]);; val it : goalstack = 1 subgoal (1 total) `!a b. ~(a < b)`
# e(SEQ_IMP_REWRITE_TAC[REAL_DIV_REFL;REAL_MUL_LID;REAL_SUB_0; REAL_LT_IMP_NE]);; val it : goalstack = No subgoals