1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
\DOC PROVE
\TYPE {PROVE : ((term # tactic) -> thm)}
\SYNOPSIS
Attempts to prove a boolean term using the supplied tactic.
\KEYWORDS
apply.
\DESCRIBE
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
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.
\SEEALSO
TAC_PROOF, prove, prove_thm, VALID.
\ENDDOC
|
