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