TACTIC : tactic

Compound

• auto-tac
• book-tac
• complete-transform*-tac
• complete-transform-tac
• diy-tac
• elim-defns-tac
• go2-tac
• min-prop
• monstro-tac
• pfenning*-tac
• pfenning-tac
• pline-tac
• prop-elim-rules-tac
• prop-intro-rules-tac
• rewrite-pline-p-tac
• rewrite-pline-tac
• rewrite-sline-tac
• sline-tac
• sub=-tac

Propositional

• absurd-tac
• backchain-lemma-tac
• cases-tac
• class-disj-tac
• deduct-tac
• disj-equiv-tac
• disj-imp-tac
• econj*-tac
• econj-tac
• eneg-tac
• equiv-disj-tac
• equiv-implics-tac
• iconj*-tac
• iconj-tac
• idisj-left-tac
• idisj-right-tac
• idisj-tac
• imp-disj-tac
• implics-equiv-tac
• indirect-disj-pline-tac
• indirect-exists-pline-tac
• indirect-tac
• indirect2-tac
• ineg-tac
• mp-tac
• neg-and-elim-tac
• neg-and-plan-tac
• neg-and-sline-tac
• neg-atom-elim-tac
• neg-equal-elim-tac
• neg-exists-elim-dup-tac
• neg-exists-elim-simple-tac
• neg-imp-elim-tac
• neg-imp-plan-tac
• neg-imp-sline-tac
• neg-neg-elim-tac
• neg-neg-plan-tac
• neg-neg-sline-tac
• neg-or-elim-dup-tac
• neg-or-elim-simple-tac
• neg-or-plan-tac
• neg-or-sline-tac
• neg-univ-elim-tac
• or-lemma-left-tac
• or-lemma-right-tac
• or-lemma-tac
• prop-prim
• propositional
• pullneg-tac
• pushneg-tac
• rulep-tac
• same-tac
• subst=-backchain-lemma-tac
• truth-tac
• truthp-rewrite-plan-tac

Quantifiers

• ab-plan-tac
• ab-sline-tac
• abu-tac
• edef-tac
• egen-tac
• exists-lemma-tac
• idef-tac
• neg-exp-plan-tac
• neg-exp-sline-tac
• neg-sel-plan-tac
• neg-sel-sline-tac
• quantificational
• rulec-tac
• ruleq-plan-tac
• ruleq-sline-tac
• symsimp-tac
• ugen-tac
• ui-herbrand-tac
• ui-tac
• unnec-exp-tac

Equality

• equality-plan-tac
• equality-sline-tac
• ext=-plan-tac
• ext=-sline-tac
• leibniz=-plan-tac
• leibniz=-sline-tac
• neg-equal-sline-tac
• refl=-tac
• subst=-tac
• subst=l-tac
• subst=r-tac
• sym=-tac

Definitions

• equiv-wffs-plan-tac
• equiv-wffs-sline-tac
• neg-rew-plan-tac
• neg-rew-sline-tac

Lambda

• beta-eta-separate-tac
• beta-eta-together-tac
• beta-only-tac
• equiv-eq-contr-tac
• equiv-eq-expd-tac
• ext=-tac
• ext=0-tac
• lcontr*-beta-tac
• lcontr*-eta-tac
• lcontr*-tac
• lcontr*-vary-tac
• lexpd*-beta-tac
• lexpd*-eta-tac
• lexpd*-tac
• lexpd*-vary-tac

Auxiliary

• finished-p
• iness-pline-tac
• make-nice
• make-room
• neg-pline-p-tac
• neg-sline-p-tac
• restrict-mating-tac
• rewrite-sline-p-tac
• show-current-plan
• show-plans
• universal-goal-p
• unsponsor-tac
• use-rulep-tac
• use-symsimp-tac

TPS documentation homepage

TPS homepage