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

EVERY_TCL : thm_tactical list -> thm_tactical

SYNOPSIS

Composes a list of theorem-tacticals.

DESCRIPTION

When given a list of theorem-tacticals and a theorem, EVERY_TCL simply composes their effects on the theorem. The effect is:

   EVERY_TCL [ttl1;...;ttln] = ttl1 THEN_TCL ... THEN_TCL ttln

In other words, if:

   ttl1 ttac th1 = ttac th2  ...  ttln ttac thn = ttac thn'

then:

   EVERY_TCL [ttl1;...;ttln] ttac th1 = ttac thn'

If the theorem-tactical list is empty, the resulting theorem-tactical behaves in the same way as ALL_THEN, the identity theorem-tactical.

FAILURE CONDITIONS

The application to a list of theorem-tacticals never fails.