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.

© 1988-99, Carnegie Mellon University.