SYM_CONV : conv
STRUCTURE
Conv
SYNOPSIS
Interchanges the left and right-hand sides of an equation.
DESCRIPTION
When applied to an equational term
t1 = t2
, the conversion
SYM_CONV
returns the theorem:
|- (t1 = t2) = (t2 = t1)
FAILURE
Fails if applied to a term that is not an equation.
SEEALSO
SYM
HOL
Kananaskis-13