NORMEQ_ss : ssfrag
STRUCTURE
SYNOPSIS
A simpset fragment that reorients equalities.
DESCRIPTION
The NORMEQ_ss simpset fragment embodies a conversion that flips terms of the form l = r when l contains no free variables, and r contains at least one variable. To flip an equality is to rewrite it so that l = r becomes r = l.
FAILURE
As a static value, this cannot fail.
EXAMPLE
In this example, the simplifier flips the 3 = x term, making it useful as a rewrite when attacking the consequent of the implication.
   SIMP_CONV (bool_ss ++ boolSimps.NORMEQ_ss) [] ``(3 = x) ==> x + 1 < y``;
   > val it =
      |- (3 = x) ==> x + 1 < y <=> (x = 3) ==> 3 + 1 < y : thm

SEEALSO
HOL  Kananaskis-13