IRULEDEF : intermediate rule definition

Collecting Help

• ab*
• abe
• absurd
• abu
• assoc-left
• beta*
• cases
• cases3
• cases4
• deduct
• disj-imp
• disj-imp-l
• disj-imp-r
• econj
• edef
• egen
• eneg
• equiv-eq
• equiv-eq-contr
• equiv-eq-contr*
• equiv-eq-expd
• equiv-eq-expd*
• equiv-implics
• equiv-wffs
• eta*
• ext=
• ext=0
• hyp
• iconj
• idef
• idisj-left
• idisj-right
• imp-disj
• imp-disj-l
• imp-disj-r
• implics-equiv
• indirect
• indirect1
• indirect2
• ineg
• lambda*
• lcontr*
• lcontr*-beta
• lcontr*-eta
• lemma
• let
• lexpd*
• lexpd*-beta
• lexpd*-eta
• mp
• pullneg
• pushneg
• rewrite-supp*
• rewrite-supp1
• rulec
• rulec1
• same
• simplify-plan
• simplify-plan*
• simplify-supp
• simplify-supp*
• subst-equiv
• subst=
• subst=l
• subst=r
• substitute
• sym=
• ugen
• ui
• unrewrite-plan*
• unrewrite-plan1
• use-rrules

TPS documentation homepage

TPS homepage