/usr/share/hol88-2.02.19940316/help/ENTRIES/GSYM.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 28 29 30 31 32 33 34 35 36 | \DOC GSYM
\TYPE {GSYM : (thm -> thm)}
\SYNOPSIS
Reverses the first equation(s) encountered in a top-down search.
\KEYWORDS
rule, symmetry, equality.
\DESCRIBE
The inference rule {GSYM} reverses the first equation(s) encountered in a
top-down search of the conclusion of the argument theorem. An equation will be
reversed iff it is not a proper subterm of another equation. If a theorem
contains no equations, it will be returned unchanged.
{
A |- ..(s1 = s2)...(t1 = t2)..
-------------------------------- GSYM
A |- ..(s2 = s1)...(t2 = t1)..
}
\FAILURE
Never fails, and never loops infinitely.
\EXAMPLE
{
#ADD;;
|- (!n. 0 + n = n) /\ (!m n. (SUC m) + n = SUC(m + n))
Run time: 0.0s
#GSYM ADD;;
|- (!n. n = 0 + n) /\ (!m n. SUC(m + n) = (SUC m) + n)
}
\SEEALSO
NOT_EQ_SYM, REFL, SYM.
\ENDDOC
|