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