DIY : MEXPR

DIY is a top-level command.
DO IT YOURSELF. Calls matingsearch procedure specified by the flag
DEFAULT-MS with specified planned line and supports, then translates the
resulting proof to natural deduction. Allows some of the output to be sent to
a separate vpform window (equivalent to issuing the OPEN-MATEVPW command
before typing DIY).
The command format for DIY is:

 <n>DIY   GOAL       SUPPORT   WINDOW 
"PLINE" "EXISTING-LINELIST" "YESNO"


The arguments have the following meaning:
GOAL : Planned Line
SUPPORT : Support Lines
WINDOW : Open Vpform Window?

TPS documentation homepage


DIY : TPS-FILE

DIY is a file.
Defines functions for calling matingsearch on current planned line.
/home/theorem/tps/lisp/diy.lisp is part of module ETR-NAT.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage