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, VALID.
\ENDDOC
|
