wlog_then : term quotation -> term quotation list -> thm_tactic -> tactic
STRUCTURE
SYNOPSIS
Apply a theorem-tactic using a proposition that can be assumed without loss of generality.
DESCRIPTION
Like wlog_tac, but the theorem P |- P is passed to the user-provided theorem-tactic instead of strip_assume_tac.
FAILURE
Never fails when applied to a theorem-tactical. The resulting tactic fails if and only if the user-provided theorem-tactical fails when used as a tactic (i.e.: when applied to a theorem and a goal).
SEEALSO
HOL  Trindemossen-1