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
concl : thm -> term
SYNOPSIS
Returns the conclusion of a theorem.
DESCRIPTION
When applied to a theorem A |- t, the function concl returns t.
FAILURE CONDITIONS
Never fails.
EXAMPLE
# ADD_SYM;;
val it : thm = |- !m n. m + n = n + m
# concl ADD_SYM;;
val it : term = `!m n. m + n = n + m`
# concl (ASSUME `1 = 0`);;
val it : term = `1 = 0`