SYMSIMP-TAC : TACTIC

SYMSIMP-TAC is a tactic.
As defined for use ETREE-NAT:
(ORELSE EXISTS-LEMMA-TAC OR-LEMMA-TAC)
Pfenning's symmetric simplification tactics.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage