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
ABS : term -> thm -> thm
SYNOPSIS
Abstracts both sides of an equation.
DESCRIPTION
A |- t1 = t2
------------------------ ABS `x` [Where x is not free in A]
A |- (\x.t1) = (\x.t2)
FAILURE CONDITIONS
If the theorem is not an equation, or if the variable x is free in the
assumptions A.
EXAMPLE
# ABS `m:num` (REFL `m:num`);;
val it : thm = |- (\m. m) = (\m. m)
COMMENTS
This is one of HOL Light's 10 primitive inference rules.