∧の導入（INTRO）と消去（ELIM）の推論には，以下の４通りがあります． |- |- ∧|- |-∧ −−−−−−−− −−−−− |- |- |- LCE CONJUNCT1,CONJUNCT2,CONJ_PAIR,CONJUNCTS |- または |- |- |- −−−−−−−−− −−−−− ∧|- |-∧ ADD_ASSUM,LCI CONJ # let LCE th1 th2 th12 = PRO…

Revision: r154 で新規実装された４つのTactic HYP DESTRUCT_TAC FIX_TAC INTRO_TAC は（鶏風ではありますが）ラベリングには便利です．例えば，GEN_TACやDISCH_TAC，DISJ*_TACの働きを有するのが INTRO_TAC http://www.cl.cam.ac.uk/~jrh13/hol-light/HTML/…