/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 | \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
|