/usr/share/hol88-2.02.19940316/help/ENTRIES/prove.doc is in hol88-help 2.02.19940316-35.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 27 | \DOC prove
\TYPE {prove : ((term # tactic) -> thm)}
\SYNOPSIS
Attempts to prove a boolean term using the supplied tactic.
\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.
\COMMENTS
The function {PROVE} provides almost identical functionality, and will
also list unsolved goals if the tactic fails. It is therefore preferable
for most purposes.
\SEEALSO
PROVE, prove_thm, TAC_PROOF, VALID.
\ENDDOC
|