HIGHER_REWRITE_CONV : thm list -> bool -> term -> thm
# COND_ELIM_THM;; val it : thm = |- P (if c then x else y) <=> (c ==> P x) /\ (~c ==> P y)
# let t = `z = if x = 0 then if y = 0 then 0 else x + y else x + y`;; val t : term = `z = (if x = 0 then if y = 0 then 0 else x + y else x + y)`
# HIGHER_REWRITE_CONV[COND_ELIM_THM] true t;; val it : thm = |- z = (if x = 0 then if y = 0 then 0 else x + y else x + y) <=> (x = 0 ==> z = (if y = 0 then 0 else x + y)) /\ (~(x = 0) ==> z = x + y)
# HIGHER_REWRITE_CONV[COND_ELIM_THM] false t;; val it : thm = |- z = (if x = 0 then if y = 0 then 0 else x + y else x + y) <=> (y = 0 ==> z = (if x = 0 then 0 else x + y)) /\ (~(y = 0) ==> z = (if x = 0 then x + y else x + y))