COND_CASES_TAC : tactic
A ?- t ========================================== COND_CASES_TAC A u {p} ?- t[T/p; u/(if p then u else v)] A u {~p} ?- t[F/p; v/(if p then u else v)]
# g `!x y:real. x <= max x y`;; val it : goalstack = 1 subgoal (1 total) `!x y. x <= max x y` # e(REPEAT GEN_TAC THEN REWRITE_TAC[real_max]);;' val it : goalstack = 1 subgoal (1 total) `x <= (if x <= y then y else x)` # e COND_CASES_TAC;; val it : goalstack = 1 subgoal (1 total) 0 [`~(x <= y)`] `x <= x`