Lines Matching defs:INT
1192 val INT =
1193 store_thm("INT",
1203 EXISTS_TAC (Term `&n:int`) THEN ASM_REWRITE_TAC[INT] THEN
1210 [INT, INT_LE_RADD, ZERO_LESS_EQ, LESS_EQ_MONO, INT_LE_REFL] THEN
1244 INDUCT_TAC THEN REWRITE_TAC[INT, ADD, INT_ADD_LID]
1252 INDUCT_TAC THEN REWRITE_TAC[INT_MUL_LZERO, MULT_CLAUSES, INT,
1278 GEN_TAC THEN REWRITE_TAC[num_CONV (Term `2n`), INT] THEN
1550 SIMP_TAC int_ss [INT] THEN GEN_TAC THEN CONJ_TAC THENL [
1567 SIMP_TAC int_ss [INT, INT_NEG_ADD, INT_LT_ADDNEG2] THEN
1569 SIMP_TAC int_ss [INT, INT_LT_ADD_SUB, int_sub, GSYM INT_NEG_ADD] THEN