CustomTokenizer/vocab.txt

<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
_
##U
##B
##G
##O
##A
##L
##_
##T
##H
##E
##N
##P
##C
##M
##I
##S
##J
##R
##W
##2
##F
##D
##.
##Q
##Y
##V
##1
##X
##_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
##UC
##T_TAC
##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
##PEC
##SPEC
Q.SPEC
Q.SPEC_TAC
ALL_TAC
EXISTS_TAC
RES_TAC
##AL
BET
##GO
##A_TAC
BETA_TAC
##GOAL
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
##UL
##OS_TAC
##_P
##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
##T_ON
##T_CASES_TAC
##ER
##RUC
##ACCEPT_TAC
ASM_CASES_TAC
STRUC
INDUCT_ON
FIRST_ASSUM
MATCH_ACCEPT_TAC
ACCEPT_TAC
STRUCT_CASES_TAC
AP
NT
##ALL_TAC
##_ALL_TAC
##M_TAC
##FF
CASES_TAC
SUFF
SUBST_ALL_TAC
NTAC
SUFF_TAC
Q_TAC
##CON
##_TER
SUBGOAL_THEN
AP_TER
AP_TERM_TAC
KN
UND
##OW_TAC
##CE_
##REWRIT
##ISCH
COND
##E_CON
ONCE_
KNOW_TAC
UNDISCH
##REWRITE_CON
ONCE_REWRITE_CON
UNDISCH_TAC
ONCE_REWRITE_CONV
AB
MA
RE
X_
##BR
##GEN_TAC
##AN
##L_TAC
##_E
##_X
##TIS
##EV
##EV_TAC
##N_E
##PAT
##RUL
##FL_TAC
##Q_TH
##YM_
##P_EV
Q.PAT
DISJ_TAC
FUN_E
SUBGOAL
SUBST_TAC
IMP_AN
FIRST_X
##ERY
COND_CASES_TAC
ABBR
MAP_EV
REFL_TAC
X_GEN_TAC
##TISYM_
##RULE
##Q_THM
Q.PAT_ASSUM
FUN_EQ_THM
SUBGOAL_TAC
IMP_ANTISYM_
FIRST_X_ASSUM
ABBREV_TAC
MAP_EVERY
IMP_ANTISYM_RULE