EDOP : editor command

Top Levels

• leave
• noop
• ok

Printing

• p
• pp
• ps
• pt

Weak Labels

• cw
• delweak
• dw
• dw*
• name
• rw

Saving Wffs

• save

Recording

• o
• rem

Vpforms

• cjform
• djform
• num-hpaths
• num-vpaths
• pj
• prop-cjform
• vp
• vpd
• vpf
• vpt

Moving Commands

• 0
• a
• d
• fb
• fi
• l
• r
• undo
• xtr
• ^

Changing Commands

• asrb
• assl
• assr
• cmrg
• cmut
• cntop
• dist-ctr
• dist-exp
• dl
• dneg
• dr
• mrg
• pmut
• subeq
• subim

Recursively Changing Commands

• asrb*
• assl*
• assr*
• cmrg*
• cmut*
• dist-ctr*
• dist-exp*
• dneg*
• mrg*
• pmut*
• subeq*
• subim*

Embedding Commands

• mbed-al
• mbed-ar
• mbed-e
• mbed-e1
• mbed-f
• mbed-il
• mbed-ir
• mbed-l
• mbed-ol
• mbed-or
• mbed-ql
• mbed-qr
• mbed=l
• mbed=r

Rewriting commands

• arr
• arr*
• arr1
• arr1*
• make-rrule
• unarr
• unarr*
• unarr1
• unarr1*

Substitution

• ab
• ib
• prim-subst
• rew-equiv
• rp
• rpall
• sub
• subst
• substyp

Basic Abbreviations

• abbr
• constants
• expand=
• expand=*
• inst
• inst1
• install
• lib-abbr
• new-defs

Lambda-Calculus

• abnorm
• etab
• etac
• etan
• etax
• leta
• lexp
• lnorm
• lnorm-beta
• lnorm-eta
• red
• ulnorm

Negation movers

• neg
• nnf
• pull-neg
• push-neg

Primitive Substitutions

• name-prim
• prt-prim

Miscellaneous

• clause-form
• cnf
• head
• hvars
• min-scope
• subformulas

RuleP

• sat
• valid

Skolemizing

• sk1
• sk3

Quantifier Commands

• db
• ep
• op

Wellformedness

• dupw
• edill
• ill
• tp
• wffp

TPS documentation homepage

TPS homepage