TARGET_REWRITE_TAC : thm list -> thm -> tactic
# REAL_ADD_RINV;; val it : thm = |- !x. x + --x = &0 # g `!x y z. --y + x + y = &0`;; Warning: inventing type variables val it : goalstack = 1 subgoal (1 total) `!x y z. --y + x + y = &0` # e(TARGET_REWRITE_TAC[REAL_ADD_AC] REAL_ADD_RINV);; val it : goalstack = 1 subgoal (1 total) `!x. x + &0 = &0`
# REAL_MUL_RINV;; val it : thm = |- !x. ~(x = &0) ==> x * inv x = &1 # g `!x y. inv y * x * y = x`;; Warning: inventing type variables val it : goalstack = 1 subgoal (1 total) `!x y z. inv y * x * y = x` # e(TARGET_REWRITE_TAC[REAL_MUL_AC] REAL_MUL_RINV);; val it : goalstack = 1 subgoal (1 total) `!x y. x * &1 = x / ~(y = &0)`
# g `!z. norm (cnj z) = norm z`;; val it : goalstack = 1 subgoal (1 total) `!z. norm (cnj z) = norm z`
# ARG;; val it : thm = |- !z. &0 <= Arg z /\ Arg z < &2 * pi /\ z = Cx (norm z) * cexp (ii * Cx (Arg z))
# e(TARGET_REWRITE_TAC[ARG] CNJ_MUL);; val it : goalstack = 1 subgoal (1 total) `!z. norm (cnj (Cx (norm z)) * cnj (cexp (ii * Cx (Arg z)))) = norm z`