Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
SYM_CONV : term -> thm
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 CONDITIONS
Fails if applied to a term that is not an equation.
EXAMPLE
# SYM_CONV `2 = x`;;
val it : thm = |- 2 = x <=> x = 2