/usr/share/hol88-2.02.19940316/help/ENTRIES/MP.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 MP
\TYPE {MP : (thm -> thm -> thm)}
\SYNOPSIS
Implements the Modus Ponens inference rule.
\KEYWORDS
rule, modus ponens, implication.
\DESCRIBE
When applied to theorems {A1 |- t1 ==> t2} and {A2 |- t1},
the inference rule {MP} returns the theorem {A1 u A2 |- t2}.
{
A1 |- t1 ==> t2 A2 |- t1
---------------------------- MP
A1 u A2 |- t2
}
\FAILURE
Fails unless the first theorem is an implication whose antecedent is the
same as the conclusion of the second theorem (up to alpha-conversion).
\SEEALSO
EQ_MP, LIST_MP, MATCH_MP, MATCH_MP_TAC, MP_TAC, NOT_MP.
\ENDDOC
|