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
TAC_PROOF : goal * tactic -> thm
SYNOPSIS
Attempts to prove a goal using a given tactic.
DESCRIPTION
When applied to a goal-tactic pair (A ?- t,tac), the TAC_PROOF function
attempts to prove the goal A ?- t, using the tactic tac. If it succeeds, it
returns the theorem A' |- t corresponding to the goal, where the assumption
list A' may be a proper superset of A unless the tactic is valid; there
is no inbuilt validity checking.
FAILURE CONDITIONS
Fails unless the goal has hypotheses and conclusions all of type bool,
and the tactic can solve the goal.