WFFREC% : recursive wff function

Top Levels

• edsearch

OTL Object

• meta-subst
• meta-subst1

Printing

• printwff

wff Primitives

• free-vars
• make-wffschema1

Equality between Wffs

• wffeq-ab1
• wffeq-def1
• wffeq-lnorm1
• wffeq-nnf1

Predicates on Wffs

• gwff-q
• legal-type-p1
• s-s-o-rec

Moving Commands

• nth-prefix-arg

Substitution

• do-primsub-rec
• replace-equiv-wff
• subst-l-term-rec

Basic Abbreviations

• instantiate-=
• instantiate-definitions

Lambda-Calculus

• lexpd-rec
• prepare-for

Quantifier Commands

• openwffa1
• openwffe1

TPS documentation homepage

TPS homepage