. 1 2 A B C D E F G H I J K L M N O P Q R S T U V W X Y _ ##E ##T ##I ##S ##_ ##A ##C ##O ##M ##H ##P ##N ##J ##F ##L ##2 ##U ##B ##W ##R ##Y ##G ##Q ##D ##. ##X ##1 ##V ##_T ##AC ##_TAC ##P_TAC ##E_TAC ##RI ##MP_TAC ##EW ##RIT ##EWRIT ##EWRITE_TAC ##W_TAC ##IMP_TAC AS ##AS ##IS ##CH ##M_ ASM_ REWRITE_TAC ##SIMP_TAC RW_TAC ##SU ##S_TAC ##ON ##SUM ST STRI ##EN ##REWRITE_TAC STRIP_TAC ##P_ SR SRW_TAC MP_TAC PR ##OV PROV PROVE_TAC CAS ##LL ##AT ##ASSUM ##ATCH ##ATCH_ ASM_SIMP_TAC Q. ##ATCH_MP_TAC ##P_ASSUM DIS ASM_REWRITE_TAC ##EN_TAC GEN_TAC DISCH FU PO SIMP_TAC POP_ASSUM MATCH_MP_TAC ##_SIMP_TAC ##LL_SIMP_TAC FULL_SIMP_TAC ##_ON ##TS_TAC ##XIS ##XISTS_TAC CASE ##S_ON CASES_ON CON ##ES_TAC ##E_ ##EXISTS_TAC Q.EXISTS_TAC SU ##ET ##_TH ##ST ##_THEN SUB ##E_REWRITE_TAC ##EC DISCH_TAC SUBST ##CE_REWRITE_TAC ASSUM ASSUME_TAC ##1_TAC SUBST1_TAC ON IM IMP_ MET ##IS_TAC ONCE_REWRITE_TAC METIS_TAC ##RES_TAC IMP_RES_TAC ##T_TAC ##UC ##V_TAC DISCH_THEN CONV_TAC ##ND CASE_TAC EQ IND EQ_TAC INDUC ##J_TAC CONJ_TAC INDUCT_TAC ##LL_TAC DEC ##ID DECID DECIDE_TAC ##SP Q.SP Q.SPEC Q.SPEC_TAC ALL_TAC EXISTS_TAC RES_TAC ##AL BET ##A_TAC ##OAL ##GOAL BETA_TAC HO ##_M HO_M ##GOAL_THEN PU ##CAS PUR ##BGOAL_THEN ##SUBGOAL_THEN Q.SUBGOAL_THEN ##CASES_TAC HO_MATCH_MP_TAC ##EP ##CEP ##CEPT_TAC FR ##_P ##OS_TAC ##UL ##AC_P FRAC_P FRAC_POS_TAC ##_ASSUM RUL ##E_ON STRIP_ASSUM ##ASSUM_TAC ##E_ASSUM_TAC PURE_ON RULE_ASSUM_TAC STRIP_ASSUME_TAC PURE_ONCE_REWRITE_TAC FI ##_CASES_TAC ##RST FIRST MATCH_ ##ATCH_TAC HO_MATCH_TAC PURE_REWRITE_TAC AC ##ER ##T_ON ##T_CASES_TAC ##RUC ##ACCEPT_TAC ASM_CASES_TAC STRUC INDUCT_ON FIRST_ASSUM MATCH_ACCEPT_TAC ACCEPT_TAC STRUCT_CASES_TAC AP NT ##_A ##M_TAC ##FF CASES_TAC SUFF SUBST_A NTAC SUFF_TAC SUBST_ALL_TAC Q_TAC ##CON ##_TER SUBGOAL_THEN AP_TER AP_TERM_TAC KN UND ##CE_ ##OW_TAC ##REWRIT ##ISCH COND ##E_CON ONCE_ KNOW_TAC UNDISCH ##REWRITE_CON ONCE_REWRITE_CON UNDISCH_TAC ONCE_REWRITE_CONV AB MA RE X_ ##EQ ##EV ##EV_TAC ##TIS ##_X ##_EQ ##AN ##PAT ##N_EQ ##FL ##BR ##RUL ##YM_ ##GEN_TAC ##P_EV Q.PAT DISJ_TAC FUN_EQ ##_THM SUBGOAL SUBST_TAC IMP_AN FIRST_X ##ERY COND_CASES_TAC ABBR MAP_EV REFL X_GEN_TAC ##TISYM_ ##RULE Q.PAT_ASSUM FUN_EQ_THM SUBGOAL_TAC IMP_ANTISYM_ FIRST_X_ASSUM ABBREV_TAC MAP_EVERY REFL_TAC IMP_ANTISYM_RULE