ML-ETR-TACTICS : MODULE

ML-ETR-TACTICS is a module.

It is loaded.
Defines tactics for translating between expansion proofs and
natural deduction proofs using math logic II rules.

NEEDED-MODULES ETR-NAT MATH-LOGIC-2-RULES

FILES ML-ETR-TACTICS-MAIN ML-ETR-TACTICS-PLINE ML-ETR-TACTICS-SLINE ML-ETR-TACTICS-BOOK ML-ETR-TACTICS-EQ ML-ETR-TACTICS-NEG ML-ETR-TACTICS-SYMSIMP ML-ETR-TACTICS-SYMSIMP2 ML-NAT-ETR1 ML-NAT-ETR2 HX-NATREE-TOP HX-NATREE-DUPLICATION HX-NATREE-RULEP HX-NATREE-AUX HX-NATREE-CLEANUP HX-NATREE-DEBUG

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage