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
prove : term * tactic -> thm
SYNOPSIS
Attempts to prove a boolean term using the supplied tactic.
DESCRIPTION
When applied to a term-tactic pair (tm,tac), the function prove attempts to
prove the goal ?- tm, that is, the term tm with no assumptions, using the
tactic tac. If prove succeeds, it returns the corresponding theorem
A |- tm, where the assumption list A may not be empty if the tactic is
invalid; prove has no inbuilt validity-checking.
FAILURE CONDITIONS
Fails if the term is not of type bool (and so cannot possibly be
the conclusion of a theorem), or if the tactic cannot solve the goal.
In the latter case prove will list the unsolved goals to help the user.