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
NO_THEN : thm_tactical
SYNOPSIS
Theorem-tactical which always fails.
DESCRIPTION
When applied to a theorem-tactic and a theorem, the theorem-tactical
NO_THEN always fails with Failwith "NO_THEN".
FAILURE CONDITIONS
Always fails when applied to a theorem-tactic and a theorem (note that it
never gets as far as being applied to a goal!)