<s> | |
<pad> | |
</s> | |
<unk> | |
<mask> | |
. | |
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 | |