REFL=-TAC is a tactic.
As defined for use NAT-DED: is a primitive tactic.
Applies rule for reflexivity of equality if planned line is of
form a=a.
As defined for use ETREE-NAT: is a primitive tactic.
If the planned line is a rewrite node with justification REFL=, applies
the ASSERT rule for reflexivity of equality. See Pfenning's theorem 141.1.

TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage